totallySeparatedSpace_of_cardinalMk_lt_continuum

English

If a topological space X has cardinality strictly less than the continuum and is completely regular (T35Space), then X is totally separated.

Русский

Если кардинал множества точек пространства X меньше континуума и пространство полностью регулярно, то оно полностью раздельно.

LaTeX

$$$\\text{Cardinal}(X) < \\mathfrak{c} \\Rightarrow \\text{TotallySeparatedSpace}(X)$ (under the given regularity assumptions).$$

Lean4

theorem totallySeparatedSpace_of_cardinalMk_lt_continuum (h : Cardinal.mk X < Cardinal.continuum) :
    TotallySeparatedSpace X :=
  totallySeparatedSpace_of_t0_of_basis_clopen <|
    CompletelyRegularSpace.isTopologicalBasis_clopens_of_cardinalMk_lt_continuum h

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