comp_assoc — Mathlib

English

Reiterating associativity of composition for multiple morphisms.

Русский

Повторное утверждение ассоциативности композиции для нескольких морфизмов.

LaTeX

$$$\\forall \\phi_1:\\, B \\to_{R}^{\\!c} C, \\; \\phi_2:\\, A \\to_{R}^{\\!c} B, \\; \\phi_3:\\, D \\to_{R}^{\\!c} A,\\; (\\phi_1.comp \\phi_2).comp \\phi_3 = \\phi_1.comp(\\phi_2.comp \\phi_3)$$$

Lean4

theorem comp_assoc (φ₁ : C →ₐc[R] D) (φ₂ : B →ₐc[R] C) (φ₃ : A →ₐc[R] B) :
    (φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃) :=
  ext fun _x => rfl

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