comp_assoc — Mathlib

English

Composition in the SmallHom construction is associative: (α ∘ β) ∘ γ = α ∘ (β ∘ γ).

Русский

Операция композиции в SmallHom ассоциативна: (α ∘ β) ∘ γ = α ∘ (β ∘ γ).

LaTeX

$$$(\alpha \circ \beta) \circ \gamma = \alpha \circ (\beta \circ \gamma)$$$

Lean4

@[simp]
theorem comp_assoc [HasSmallLocalizedHom.{w} W X Y] [HasSmallLocalizedHom.{w} W X Z] [HasSmallLocalizedHom.{w} W X T]
    [HasSmallLocalizedHom.{w} W Y Z] [HasSmallLocalizedHom.{w} W Y T] [HasSmallLocalizedHom.{w} W Z T]
    (α : SmallHom.{w} W X Y) (β : SmallHom.{w} W Y Z) (γ : SmallHom.{w} W Z T) :
    (α.comp β).comp γ = α.comp (β.comp γ) := by
  apply (equiv W W.Q).injective
  simp only [equiv_comp, assoc]

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