stoneCechExtend_extends — Mathlib

English

For all a ∈ α, stoneCechExtend hg (stoneCechUnit a) = g a.

Русский

Для каждого a ∈ α выполняется stoneCechExtend hg (stoneCechUnit a) = g a.

LaTeX

$$$ \forall a:\alpha,\; stoneCechExtend hg (stoneCechUnit a) = g a $$$

Lean4

@[simp]
theorem stoneCechExtend_extends : stoneCechExtend hg ∘ stoneCechUnit = g :=
  by
  ext x
  rw [stoneCechExtend, Function.comp_apply, stoneCechUnit, T2Quotient.lift_mk]
  apply congrFun (preStoneCechExtend_extends hg)

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