denseRange_stoneCechUnit — Mathlib

English

The image of α under the natural map stoneCechUnit is dense in StoneCech α.

Русский

Образ α под натуральной картой stoneCechUnit плотно заполнен в StoneCech α.

LaTeX

$$$ DenseRange( stoneCechUnit ) $$$

Lean4

/-- The image of `stoneCechUnit` is dense. (But `stoneCechUnit` need
  not be an embedding, for example if the original space is not Hausdorff.) -/
theorem denseRange_stoneCechUnit : DenseRange (stoneCechUnit : α → StoneCech α) :=
  by
  unfold stoneCechUnit T2Quotient.mk
  have : Function.Surjective (T2Quotient.mk : PreStoneCech α → StoneCech α) := by exact Quot.mk_surjective
  exact this.denseRange.comp denseRange_preStoneCechUnit continuous_coinduced_rng

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