toBasis_toOrthonormalBasis — Mathlib

English

The operation to construct an orthonormal basis from a basis preserves the underlying vector assignments.

Русский

Операция построения ортонормированного базиса из базиса сохраняет сопоставления векторов.

LaTeX

$$$v.toOrthonormalBasis hv = ...$$$

Lean4

@[simp]
theorem _root_.Module.Basis.toBasis_toOrthonormalBasis (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
    (v.toOrthonormalBasis hv).toBasis = v := by simp [Basis.toOrthonormalBasis, OrthonormalBasis.toBasis]

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