isDenseEmbedding_stoneCechUnit — Mathlib

English

The Stone–Čech embedding stoneCechUnit is a dense embedding of X into StoneCech X.

Русский

Встраивание Stone–Čech, отображение stoneCechUnit, является плотным вложением пространства X в StoneCech X.

LaTeX

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

Lean4

theorem isDenseEmbedding_stoneCechUnit [T35Space X] : IsDenseEmbedding (stoneCechUnit : X → StoneCech X)
    where
  toIsDenseInducing := isDenseInducing_stoneCechUnit
  injective := injective_stoneCechUnit_of_t35Space

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