map_equiv — Mathlib

English

If hv is an orthonormal basis and hv' is an orthonormal basis, then mapping via the equivalence (hv.equiv hv' e).toLinearEquiv yields the same as the reindexed hv'.

Русский

Если hv — ортонормированный базис, hv' — ортонормированный базис, то отображение через эквивалентность даёт тот же базис, что и переразнесение hv'.

LaTeX

$$Eq (v.map (hv.equiv hv' e).toLinearEquiv) (v'.reindex e.symm)$$

Lean4

theorem map_equiv {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 v') (e : ι ≃ ι') :
    v.map (hv.equiv hv' e).toLinearEquiv = v'.reindex e.symm :=
  v.map_equiv _ _

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