linearIsometryEquiv_symm_apply_single_one

English

An orthonormal family with dense span forms a Hilbert sum decomposing E as the direct sum of line spans.

Русский

Ортонормированная семья с плотной областью развёртывания образует гильбертову сумму, разлагающую E на прямую сумму линейных отрезков.

LaTeX

$$$ IsHilbertSum 𝕜 (ι \\to 𝕜) (\\lambda i, LinearIsometry.toSpanSingleton 𝕜 E (hv.1 i)) $$

Lean4

theorem _root_.Orthonormal.linearIsometryEquiv_symm_apply_single_one [DecidableEq ι] (h i) :
    (hv.isHilbertSum h).linearIsometryEquiv.symm (lp.single 2 i 1) = v i := by
  rw [IsHilbertSum.linearIsometryEquiv_symm_apply_single, LinearIsometry.toSpanSingleton_apply, one_smul]

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