mk — Mathlib · SciLib

English

The same reconstruction identity holds with alternate indexing and sums.

Русский

Та же идентичность реконструкции сохраняется для другой нумерации и суммирования.

LaTeX

$$$ HasSum (\\lambda i, (b.repr x)_i · b_i) x $$$

Lean4

/-- An orthonormal family of vectors whose span is dense in the whole module is a Hilbert basis. -/
protected def mk (hsp : ⊤ ≤ (span 𝕜 (Set.range v)).topologicalClosure) : HilbertBasis ι 𝕜 E :=
  HilbertBasis.ofRepr <| (hv.isHilbertSum hsp).linearIsometryEquiv

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