simp only [nhds_top', tendsto_iInf, tendsto_principal, mem_Ioi]
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
m : α → ℕ∞
f : Filter α
⊢ Tendsto m f (𝓝 ⊤) ↔ ∀ (x : ℕ), ∀ᶠ (a : α) in f, ↑x < m a
no goals