Theorem: FilterGame.TopologicalSpace.mem_nhds_def (FilterGame/Solutions/Topology.lean)

State before:
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
⊢ s ∈ 𝓝 a ↔ ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
Tactic:
exact Iff.rfl
State after:
no goals