toHilbertBasis — Mathlib

English

A finite orthonormal basis is a Hilbert basis; the associated vector function coincides with the original basis vectors.

Русский

Конечный ортонормированный базис является базисом Хилберта; соответствующая функция вектора совпадает с исходными векторами базиса.

LaTeX

$$$ (b.toHilbertBasis : \\iota \\to E) = b $$$

Lean4

/-- An orthonormal basis is a Hilbert basis. -/
protected def _root_.OrthonormalBasis.toHilbertBasis [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) : HilbertBasis ι 𝕜 E :=
  HilbertBasis.mk b.orthonormal <| by
    simpa only [← OrthonormalBasis.coe_toBasis, b.toBasis.span_eq, eq_top_iff] using @subset_closure E _ _

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