English
Discrete topology is equivalent to nhds x = pure x for all x.
Русский
Дискретная топология эквивалентна nhds x = pure x для всех x.
LaTeX
$$$DiscreteTopology(\alpha) \iff \forall x:\alpha, nhds(x) = \mathrm{pure}(x)$$$
Lean4
/-- This lemma characterizes discrete topological spaces as those whose singletons are
neighbourhoods. -/
theorem discreteTopology_iff_nhds [TopologicalSpace α] : DiscreteTopology α ↔ ∀ x : α, 𝓝 x = pure x :=
by
simp only [discreteTopology_iff_singleton_mem_nhds]
apply forall_congr' (fun x ↦ ?_)
simp [le_antisymm_iff, pure_le_nhds x]