t1Space — Mathlib

English

If X is TotallyDisconnectedSpace, then it is a T1 space.

Русский

Если X является TotallyDisconnectedSpace, тогда X является T1-пространством.

LaTeX

$$$\mathrm{TotallyDisconnectedSpace}(X) \Rightarrow \mathrm{T1Space}(X)$$$

Lean4

instance (priority := 100) t1Space [h : TotallyDisconnectedSpace X] : T1Space X :=
  by
  rw [((t1Space_TFAE X).out 0 1 :)]
  intro x
  rw [← totallyDisconnectedSpace_iff_connectedComponent_singleton.mp h x]
  exact isClosed_connectedComponent

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