no goals
α : Type u
β : Type v
γ : Type ?u.18624
δ : Type ?u.18627
ε : Type ?u.18630
ζ : Type ?u.18633
a : CofiniteTopology α
s : Set (CofiniteTopology α)
⊢ s ∈ 𝓝 a ↔ a ∈ s ∧ Set.Finite (sᶜ)
simp [nhds_eq]