comp_assoc — Mathlib

English

For order-preserving monoid homomorphisms f: γ →*o δ, g: β →*o γ, h: α →*o β, the composition is associative: (f ∘ g) ∘ h = f ∘ (g ∘ h).

Русский

Для упорядоченных моноид-гомоморфизмов f: γ →*o δ, g: β →*o γ и h: α →*o β композиция удовлетворяет ассоциативности: (f ∘ g) ∘ h = f ∘ (g ∘ h).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem comp_assoc (f : γ →*o δ) (g : β →*o γ) (h : α →*o β) : (f.comp g).comp h = f.comp (g.comp h) :=
  rfl

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