instTotallySeparatedSpaceOfCountable

English

Every countable topological space is totally separated (under the appropriate normality/regularity framework).

Русский

Каждое счетное топологическое пространство полностью раздельно при условии необходимого регуляторного предположения.

LaTeX

$$$[\\text{Countable } X] \\Rightarrow \\text{TotallySeparatedSpace } X$ (in the given setting).$$

Lean4

instance [Countable X] : TotallySeparatedSpace X :=
  totallySeparatedSpace_of_cardinalMk_lt_continuum <|
    (Cardinal.mk_le_aleph0_iff.mpr inferInstance).trans_lt Cardinal.aleph0_lt_continuum

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