trans_assoc — Mathlib

English

Composition of three pseudoequivalences 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

theorem trans_assoc (f : α ≃. β) (g : β ≃. γ) (h : γ ≃. δ) : (f.trans g).trans h = f.trans (g.trans h) :=
  ext fun _ => Option.bind_assoc _ _ _

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