equiv_toLinearEquiv — Mathlib

English

The composition of two orthonormal equivalences equals the direct equivalence corresponding to the transitive composition of index bijections.

Русский

Сложение двух ортонормированных эквивалентностей равно прямой эквивалентности, соответствующей транспитивному сопряжению индексов.

LaTeX

$$$(hv.equiv hv' e).trans (hv'.equiv hv'' e') = hv.equiv hv'' (e.trans e')$$$

Lean4

@[simp]
theorem equiv_toLinearEquiv {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 v')
    (e : ι ≃ ι') : (hv.equiv hv' e).toLinearEquiv = v.equiv v' e :=
  rfl

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