toIsometryEquiv_trans — Mathlib

English

The associative law holds for trans: composing three LinearIsometryEquiv's is associative.

Русский

Сочетательность переходов для линейных изометрических эквивалентов справедлива: (e1 trans e2) trans e3 = e1 trans (e2 trans e3).

LaTeX

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

Lean4

@[simp]
theorem toIsometryEquiv_trans (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
    (e.trans e').toIsometryEquiv = e.toIsometryEquiv.trans e'.toIsometryEquiv :=
  rfl

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