equiv_apply — Mathlib

English

If hv is orthonormal and hv' is another orthonormal basis, then mapping via hv.equiv hv' e yields the same as taking the reindexed basis of the other and confirms the equality of the mapped basis.

Русский

Если hv ортонормальна, а hv' — другая ортонормированная база, то отображение через hv.equiv hv' e даёт базис, совпадающий с переразмещённой базой hv'.

LaTeX

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

Lean4

@[simp]
theorem equiv_apply {ι' : Type*} {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 v')
    (e : ι ≃ ι') (i : ι) : hv.equiv hv' e (v i) = v' (e i) :=
  Basis.equiv_apply _ _ _ _

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