equiv_refl — Mathlib

English

For any index i, applying the orthonormal equivalence to the basis element v_i yields the corresponding v'_j under the index bijection.

Русский

Для каждого индекса i применение ортонормированной эквивалентности к базисному вектору v_i даёт соответствующий вектор v'_j под соответствием индексов.

LaTeX

$$$hv.equiv hv' e (v i) = v' (e i)$$$

Lean4

@[simp]
theorem equiv_refl {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) :
    hv.equiv hv (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E :=
  v.ext_linearIsometryEquiv fun i => by
    simp only [Orthonormal.equiv_apply, Equiv.coe_refl, id, LinearIsometryEquiv.coe_refl]

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