coe_toOrthonormalBasis — Mathlib

English

The toBasis operation applied to the orthonormalized basis recovers the original basis.

Русский

Операция toBasis после ортонормирования восстанавливает исходный базис.

LaTeX

$$$(v.toOrthonormalBasis hv).toBasis = v$$$

Lean4

@[simp]
theorem _root_.Module.Basis.coe_toOrthonormalBasis (v : Basis ι 𝕜 E) (hv : Orthonormal 𝕜 v) :
    (v.toOrthonormalBasis hv : ι → E) = (v : ι → E) :=
  calc
    (v.toOrthonormalBasis hv : ι → E) = ((v.toOrthonormalBasis hv).toBasis : ι → E) := by
      classical rw [OrthonormalBasis.coe_toBasis]
    _ = (v : ι → E) := by simp

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