stoneCechExtend — Mathlib

English

The extension composed with the canonical map equals the original map: stoneCechExtend hg ∘ stoneCechUnit = g.

Русский

Расширение, скомпонованное с канонической картой, равно исходной карте: stoneCechExtend hg ∘ stoneCechUnit = g.

LaTeX

$$$ stoneCechExtend hg \circ stoneCechUnit = g $$$

Lean4

/-- The extension of a continuous function from `α` to a compact
  Hausdorff space `β` to the Stone-Čech compactification of `α`.
  This extension implements the universal property of this compactification. -/
def stoneCechExtend : StoneCech α → β :=
  T2Quotient.lift (continuous_preStoneCechExtend hg)

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