discreteTopology_iff_nhds_ne — Mathlib

English

Discrete topology is equivalent to nhdsWithin x (X \ {x}) = ⊥ for all x.

Русский

Дискретная топология эквивалентна nhdsWithin x (X \ {x}) = ⊥ для всех x.

LaTeX

$$$DiscreteTopology(\alpha) \iff \forall x:\alpha, nhdsWithin(x, \alpha \setminus \{x\}) = \bot$$$

Lean4

theorem discreteTopology_iff_nhds_ne [TopologicalSpace α] : DiscreteTopology α ↔ ∀ x : α, 𝓝[≠] x = ⊥ := by
  simp only [discreteTopology_iff_singleton_mem_nhds, nhdsWithin, inf_principal_eq_bot, compl_compl]

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