discreteTopology_iff_singleton_mem_nhds

English

Discrete topology iff every singleton is a neighborhood of its point.

Русский

Дискретная топология эквивалентна тому, что каждое единичное множество является окрестностью своей точки.

LaTeX

$$$DiscreteTopology(\alpha) \iff \forall x:\alpha, {x} \in 𝓝 x$$$

Lean4

theorem discreteTopology_iff_singleton_mem_nhds [TopologicalSpace α] : DiscreteTopology α ↔ ∀ x : α, { x } ∈ 𝓝 x := by
  simp only [discreteTopology_iff_isOpen_singleton, isOpen_iff_mem_nhds, mem_singleton_iff, forall_eq]

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