trans_assoc — Mathlib

English

Let e12: M1 ≃ M2, e23: M2 ≃ M3, and e34: M3 ≃ M4 be linear equivalences. Then the composition is associative: (e12.trans e23).trans e34 = e12.trans (e23.trans e34).

Русский

Пусть e12: M1 ≃ M2, e23: M2 ≃ M3 и e34: M3 ≃ M4 — линейные эквивалентности. Тогда композиция эквивалентностей ассоциативна: (e12.trans e23).trans e34 = e12.trans (e23.trans e34).

LaTeX

$$$ (e_{12}.trans e_{23}).trans e_{34} = e_{12}.trans (e_{23}.trans e_{34}) $$$

Lean4

theorem trans_assoc (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) (e₃₄ : M₃ ≃ₛₗ[σ₃₄] M₄) :
    (e₁₂.trans e₂₃).trans e₃₄ = e₁₂.trans (e₂₃.trans e₃₄) :=
  rfl

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