trans_assoc — Mathlib

English

Composition of three order-monoid isomorphisms is associative: (f.trans g).trans h = f.trans (g.trans h).

Русский

Объединение трёх упорядоченных моноидных изоморфизмов ассоциативно: (f.trans g).trans h = f.trans (g.trans h).

LaTeX

$$$(f.trans g).trans h = f.trans (g.trans h)$$$

Lean4

@[to_additive (attr := simp)]
theorem trans_assoc (f : α ≃*o β) (g : β ≃*o γ) (h : γ ≃*o δ) : (f.trans g).trans h = f.trans (g.trans h) :=
  rfl

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