preStoneCechExtend_preStoneCechUnit

English

Let α be a topological space and β a compact Hausdorff space, and g: α → β be continuous. The extension to Stone–Čech α agrees with g on the canonical embedding of α, i.e. for every a ∈ α, preStoneCechExtend hg (preStoneCechUnit a) = g a.

Русский

Пусть α — топологическое пространство, β — компактное хаусдорфово, f: α → β непрерывна. Расширение до Stone-Čech α совпадает с f на каноническом отображении α, то есть для каждого a ∈ α выполняется preStoneCechExtend hg (preStoneCechUnit a) = g a.

LaTeX

$$$ preStoneCechExtend hg (preStoneCechUnit a) = g a $$$

Lean4

@[simp]
theorem preStoneCechExtend_preStoneCechUnit (a : α) : preStoneCechExtend hg (preStoneCechUnit a) = g a :=
  congr_fun (preStoneCechExtend_extends hg) a

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