English
An orthonormal subset of a Hilbert space can be extended to a full Hilbert basis. More precisely, given an orthonormal set s, there exist a larger index set w and a Hilbert basis b on w such that s is included in w and b represents the inclusion of w into E.
Русский
Ортонормированное подмножество пространства Хилберта может быть дополнено до полного базиса Хилберта. Другими словами, для данного ортонормированного множества s существуют w и базис Хилберта на w, удовлетворяющие включению s в w и представлению b как инклюзии w в E.
LaTeX
$$$\\exists w\\,\\exists b:\\, HilbertBasis\,w\\,\\, 𝕜\\,E,\\ s\\subseteq w \\land \\; \\hat{b} = \\iota_w$$$
Lean4
@[simp]
theorem _root_.OrthonormalBasis.coe_toHilbertBasis [Fintype ι] (b : OrthonormalBasis ι 𝕜 E) :
(b.toHilbertBasis : ι → E) = b :=
HilbertBasis.coe_mk _ _
