completelyRegularSpace_iff_isInducing_stoneCechUnit

English

A space is completely regular iff the map to its Stone–Cech compactification is inducing.

Русский

Пространство полностью регулярное тогда и только тогда, когда отображение в компактное Стонe-Кэч соответствующее индукирует топологию.

LaTeX

$$$[CompletelyRegularSpace X] \\iff IsInducing (stoneCechUnit : X \\to StoneCech X)$$$

Lean4

theorem completelyRegularSpace_iff_isInducing_stoneCechUnit :
    CompletelyRegularSpace X ↔ IsInducing (stoneCechUnit : X → StoneCech X)
    where
  mp _ := isInducing_stoneCechUnit
  mpr hs := hs.completelyRegularSpace

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