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

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
⊢ 𝓝 ⊤ = ⨅ a, ⨅ (_ : a ≠ ⊤), 𝓟 (Ioi a)
Tactic:
simp_rw [nhds_top_order, Ioi, lt_top_iff_ne_top]
State after:
no goals