theorem Filter.Tendsto.min_atTop_atTop {α : Type u_2} {β : Type u_3} [Nonempty β] [LinearOrder β] [LinearOrder α] {f g : β → α} (hf : Tendsto f atTop atTop) (hg : Tendsto g atTop atTop) : Tendsto (fun (x : β) => min (f x) (g x)) atTop atTop

theorem WithTop.tendsto_nhds_top_iff {ι : Type u_1} {α : Type u_2} [Nonempty ι] [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] {f : Filter α} (x : α → WithTop ι) : Filter.Tendsto x f (nhds ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, ↑i < x a

theorem WithTop.tendsto_atTop_nhds_top_iff {ι : Type u_1} {α : Type u_2} [Nonempty ι] [LinearOrder ι] [TopologicalSpace ι] [OrderTopology ι] [Nonempty α] [inst : Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≤ x2] (x : α → WithTop ι) : Filter.Tendsto x Filter.atTop (nhds ⊤) ↔ ∀ (i : ι), ∃ (N : α), ∀ n ≥ N, ↑i < x n

theorem Filter.Tendsto.tendsto_withTop_atTop_nhds_top {ι : Type u_1} [Nonempty ι] [LinearOrder ι] [NoMaxOrder ι] [TopologicalSpace ι] [OrderTopology ι] {a : ℕ → ι} (ha : Tendsto a atTop atTop) : Tendsto (fun (n : ℕ) => ↑(a n)) atTop (nhds ⊤)