trans_assoc — Mathlib

English

Associativity of trans: (e1.trans e2).trans e3 = e1.trans (e2.trans e3).

Русский

Ассоциативность композиции: (e1.trans e2).trans e3 = e1.trans (e2.trans e3).

LaTeX

$$$((e_1 \text{ trans } e_2) \text{ trans } e_3) = (e_1 \text{ trans } (e_2 \text{ trans } e_3))$$$

Lean4

theorem trans_assoc (e₁ : P₁ ≃ᴬ[k] P₂) (e₂ : P₂ ≃ᴬ[k] P₃) (e₃ : P₃ ≃ᴬ[k] P₄) :
    (e₁.trans e₂).trans e₃ = e₁.trans (e₂.trans e₃) :=
  ext fun _ ↦ rfl

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