toOrthonormalBasis — Mathlib

English

A finite Hilbert basis is an orthonormal basis.

Русский

Конечная гильбертова база является ортонормированной базой.

LaTeX

$$$ b.\\text{toOrthonormalBasis} = \\text{orthonormal basis of } E $$$

Lean4

/-- A finite Hilbert basis is an orthonormal basis. -/
protected def toOrthonormalBasis [Fintype ι] (b : HilbertBasis ι 𝕜 E) : OrthonormalBasis ι 𝕜 E :=
  OrthonormalBasis.mk b.orthonormal
    (by
      refine Eq.ge ?_
      classical
      have := (span 𝕜 (Finset.univ.image b : Set E)).closed_of_finiteDimensional
      simpa only [Finset.coe_image, Finset.coe_univ, Set.image_univ, HilbertBasis.dense_span] using
        this.submodule_topologicalClosure_eq.symm)

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