comp_assoc — Mathlib

English

Composition of coalgebra homomorphisms is associative: (φ1 ∘ φ2) ∘ φ3 = φ1 ∘ (φ2 ∘ φ3).

Русский

Композиция коалгоморфизмов ассоциативна: (φ1 ∘ φ2) ∘ φ3 = φ1 ∘ (φ2 ∘ φ3).

LaTeX

$$$(\varphi_1 \circ \varphi_2) \circ \varphi_3 = \varphi_1 \circ (\varphi_2 \circ \varphi_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

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