comp_assoc — Mathlib

English

Let f: M1 → SL[σ12] M2, g: M2 → SL[σ23] M3, h: M3 → SL[σ34] M4 be continuous linear maps. Then (h ∘ g) ∘ f = h ∘ (g ∘ f).

Русский

Пусть f: M1 → SL[σ12] M2, g: M2 → SL[σ23] M3, h: M3 → SL[σ34] M4 — непрерывные линейные отображения. Тогда (h ∘ g) ∘ f = h ∘ (g ∘ f).

LaTeX

$$$ (h \circ g) \circ f = h \circ (g \circ f) $$$

Lean4

theorem comp_assoc {R₄ : Type*} [Semiring R₄] [Module R₄ M₄] {σ₁₄ : R₁ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
    [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (h : M₃ →SL[σ₃₄] M₄)
    (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : (h.comp g).comp f = h.comp (g.comp f) :=
  rfl

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