Theorem: ENat.tendsto_nhds_top_iff (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : 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
Tactic:
simp only [nhds_top', tendsto_iInf, tendsto_principal, mem_Ioi]
State after:
no goals