compStarAlgHom'_comp — Mathlib

English

The composition of precomposition by g and by f equals precomposition by the composition g ∘ f: compStarAlgHom'(𝕜,A,g ∘ f) = compStarAlgHom'(𝕜,A,f) ∘ compStarAlgHom'(𝕜,A,g).

Русский

Составление предсоставления двумя отображениями даёт предсоставление композиции: compStarAlgHom'(𝕜,A,g ∘ f) = compStarAlgHom'(𝕜,A,f) ∘ compStarAlgHom'(𝕜,A,g).

LaTeX

$$$\operatorname{compStarAlgHom}'(g\circ f) = (\operatorname{compStarAlgHom}'(f))\circ (\operatorname{compStarAlgHom}'(g))$$$

Lean4

/-- `ContinuousMap.compStarAlgHom'` is functorial. -/
theorem compStarAlgHom'_comp (g : C(Y, Z)) (f : C(X, Y)) :
    compStarAlgHom' 𝕜 A (g.comp f) = (compStarAlgHom' 𝕜 A f).comp (compStarAlgHom' 𝕜 A g) :=
  StarAlgHom.ext fun _ => ContinuousMap.ext fun _ => rfl

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