coe_toOrthonormalBasis_repr_symm — Mathlib

English

A basis with orthonormality yields an orthonormal basis via the provided construction.

Русский

Базис, обладающий ортонормированностью, порождает ортонормированный базис через данную конструкцию.

LaTeX

$$Definition: (v : Basis ι 𝕜 E) with hv ⇒ (v.toOrthonormalBasis hv) is ONB$$

Lean4

@[simp]
theorem _root_.Module.Basis.coe_toOrthonormalBasis_repr_symm (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
    ((v.toOrthonormalBasis hv).repr.symm : EuclideanSpace 𝕜 ι → E) = v.equivFun.symm :=
  rfl

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