closedPoints_eq_univ — Mathlib

English

If X is a T1 space, then every point x is closed as a singleton, hence closedPoints X equals the whole space.

Русский

Если пространство T1, то каждое множество {x} замкнуто, следовательно closedPoints X = univ.

LaTeX

$$$[T1Space X] \Rightarrow closedPoints X = \mathrm{Set.univ}$$$

Lean4

theorem closedPoints_eq_univ [T1Space X] : closedPoints X = Set.univ :=
  Set.eq_univ_iff_forall.mpr fun _ ↦ isClosed_singleton

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