English
Same principle: from an orthonormal subset s, there exists a Hilbert basis extending it and realizing the inclusion map.
Русский
Та же идея: из ортонормированного подмножества s существует база Хилберта, расширяющая его, и реализующая включение в E.
LaTeX
$$$\\exists w\\,\\exists b : HilbertBasis\,w\\, 𝕜 E, \\, s \\subseteq w \\land \\; (b) = \\iota_w$$$
Lean4
/-- A Hilbert space admits a Hilbert basis extending a given orthonormal subset. -/
theorem _root_.Orthonormal.exists_hilbertBasis_extension {s : Set E} (hs : Orthonormal 𝕜 ((↑) : s → E)) :
∃ (w : Set E) (b : HilbertBasis w 𝕜 E), s ⊆ w ∧ ⇑b = ((↑) : w → E) :=
let ⟨w, hws, hw_ortho, hw_max⟩ := exists_maximal_orthonormal hs
⟨w,
HilbertBasis.mkOfOrthogonalEqBot hw_ortho
(by
simpa only [Subtype.range_coe_subtype, Set.setOf_mem_eq,
maximal_orthonormal_iff_orthogonalComplement_eq_bot hw_ortho] using hw_max),
hws, HilbertBasis.coe_mkOfOrthogonalEqBot _ _⟩
