coe_toOrthonormalBasis — Mathlib

English

A canonical construction yields that the representative of the basis equals the given vector function.

Русский

Каноническое отображение даёт, что образец базиса совпадает с заданной функцией векторов.

LaTeX

$$$ (b \\;\\text{to})\\;\\text{coefficients} = v $$$

Lean4

@[simp]
theorem coe_toOrthonormalBasis [Fintype ι] (b : HilbertBasis ι 𝕜 E) : (b.toOrthonormalBasis : ι → E) = b :=
  OrthonormalBasis.coe_mk _ _

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