t35Space_iff_isEmbedding_stoneCechUnit

English

For any X, T35Space X if and only if stoneCechUnit is an embedding.

Русский

Для любого X пространство T35 тогда и только тогда, когда stoneCechUnit является вложением.

LaTeX

$$$T35Space X \iff IsEmbedding(\mathrm{stoneCechUnit}: X \to \mathrm{StoneCech} X)$$$

Lean4

theorem t35Space_iff_isEmbedding_stoneCechUnit : T35Space X ↔ IsEmbedding (stoneCechUnit : X → StoneCech X)
    where
  mp _ := isEmbedding_stoneCechUnit
  mpr hs := hs.t35Space

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