equiv_symm — Mathlib

English

The inverse of an orthonormal equivalence is the orthonormal equivalence with the inverse index bijection.

Русский

Обратная ортонормированной эквивалентности равна ортонормированной эквивалентности с обратным биекцией индексов.

LaTeX

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

Lean4

@[simp]
theorem equiv_symm {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) {v' : Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 v') (e : ι ≃ ι') :
    (hv.equiv hv' e).symm = hv'.equiv hv e.symm :=
  v'.ext_linearIsometryEquiv fun i =>
    (hv.equiv hv' e).injective <| by
      simp only [LinearIsometryEquiv.apply_symm_apply, Orthonormal.equiv_apply, e.apply_symm_apply]

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