comp_assoc — Mathlib

English

Another form of associativity for composition of isometries holds identically.

Русский

Ещё одно формальное выражение ассоциативности композиции изометрий сохраняется едва ли иначе.

LaTeX

$$$\text{Eq}((h \circ g) \circ f, h \circ (g \circ f))$$$

Lean4

theorem comp_assoc (h : Q₃ →qᵢ Q₄) (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) : (h.comp g).comp f = h.comp (g.comp f) :=
  ext fun _ => rfl

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