isEmbedding_stoneCechUnit — Mathlib

English

For any X with a T35 space, the map stoneCechUnit: X → StoneCech X is an embedding.

Русский

Для пространства X с топологией T35 отображение stoneCechUnit: X → StoneCech X является вложением.

LaTeX

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

Lean4

theorem isEmbedding_stoneCechUnit [T35Space X] : IsEmbedding (stoneCechUnit : X → StoneCech X)
    where
  toIsInducing := isInducing_stoneCechUnit
  injective := injective_stoneCechUnit_of_t35Space

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