feat: Simple lemmas about convergence in WithTop (leanprover-community#33374)

Author: kex-y

Mathlib/Topology/Order/WithTop.lean

@@ -255,4 +255,21 @@ def sumHomeomorph [OrderTop ι] : WithTop ι ≃ₜ ι ⊕ Unit where
     exact Continuous.comp_continuousOn (by fun_prop) continuousOn_untopA
   continuous_invFun := continuous_sum_dom.mpr ⟨by fun_prop, by fun_prop⟩
 
+lemma tendsto_nhds_top_iff {α : Type*} {f : Filter α} (x : α → WithTop ι) :
+    Tendsto x f (𝓝 ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, i < x a := by
+  obtain (h | h) := isEmpty_or_nonempty ι
+  · simpa using .of_forall fun _ ↦ Subsingleton.elim ..
+  refine nhds_top_basis.tendsto_right_iff.trans ?_
+  rw [← Set.forall_mem_range (p := (∀ᶠ a in f, · < x a)), WithTop.range_coe]
+  simp
+
+lemma tendsto_coe_atTop [NoMaxOrder ι] :
+    Tendsto ((↑) : ι → WithTop ι) atTop (𝓝 ⊤) := by
+  obtain (h | h) := isEmpty_or_nonempty ι
+  · simpa using Subsingleton.elim ..
+  rw [tendsto_nhds_top_iff]
+  intro i
+  filter_upwards [atTop_basis_Ioi.mem_of_mem (i := i) trivial]
+  simp
+
 end WithTop