preStoneCechExtend — Mathlib

English

The extension of a continuous g along preStoneCechUnit is equal to g on the base space: preStoneCechExtend hg ∘ preStoneCechUnit = g.

Русский

Расширение непрерывной g по preStoneCechUnit совпадает с g на базовом пространстве: preStoneCechExtend hg ∘ preStoneCechUnit = g.

LaTeX

$$$preStoneCechExtend\; hg \circ preStoneCechUnit = g$$$

Lean4

/-- The extension of a continuous function from `α` to a compact
  Hausdorff space `β` to the pre-Stone-Čech compactification of `α`. -/
def preStoneCechExtend : PreStoneCech α → β :=
  Quot.lift (Ultrafilter.extend g) fun _ _ ⟨_, hF, hG⟩ ↦ preStoneCechCompat hg hF hG

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