t1Space_iff_continuous_cofinite_of

English

A space is T1 iff for every pair of distinct points x,y there exists an open set U with x ∈ U and y ∉ U.

Русский

Пространство является T1 тогда и только тогда, когда для любой пары различных точек x,y существует открытое множество U с x ∈ U и y ∉ U.

LaTeX

$$$T1Space(X) \\iff \\forall x \\forall y, x \\neq y \\Rightarrow \\exists U\\,(IsOpen(U) \\land x \\in U \\land y \\notin U).$$$

Lean4

theorem t1Space_iff_continuous_cofinite_of : T1Space X ↔ Continuous (@CofiniteTopology.of X) :=
  (t1Space_TFAE X).out 0 3

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