discreteTopology_iff_nhds — Mathlib

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]

Похожие утверждения