English
Let E be a normed inner product space and S a set of vectors in E that are orthonormal. Then there exists a maximal orthonormal set W in E containing S, i.e., W ⊇ S and W is orthonormal, and any orthonormal set U containing W must satisfy U = W.
Русский
Пусть E — нормированное внутриопределённое пространство, а S — множество векторов в E, составляющих ортонормированную систему. Существуют максимальные ортонормированные подмножества W в E, содержащие S: S ⊆ W, W ортонормированно, и любое ортонормированное множество U, содержащее W, равняется W.
LaTeX
$$$\\exists W\\,\\bigl(W \\supseteq S \\wedge \\operatorname{Orthonormal}_{\\mathbb{K}}(\\operatorname{Subtype.val}:W\\to E) \\wedge \\forall U\\supseteq W,\\ \\operatorname{Orthonormal}_{\\mathbb{K}}(\\operatorname{Subtype.val}:U\\to E)\\to U=W\\bigr).$$$
Lean4
/-- Given an orthonormal set `v` of vectors in `E`, there exists a maximal orthonormal set
containing it. -/
theorem exists_maximal_orthonormal {s : Set E} (hs : Orthonormal 𝕜 (Subtype.val : s → E)) :
∃ w ⊇ s, Orthonormal 𝕜 (Subtype.val : w → E) ∧ ∀ u ⊇ w, Orthonormal 𝕜 (Subtype.val : u → E) → u = w :=
by
have := zorn_subset_nonempty {b | Orthonormal 𝕜 (Subtype.val : b → E)} ?_ _ hs
· obtain ⟨b, hb⟩ := this
exact ⟨b, hb.1, hb.2.1, fun u hus hu => hb.2.eq_of_ge hu hus⟩
· refine fun c hc cc _c0 => ⟨⋃₀ c, ?_, ?_⟩
· exact orthonormal_sUnion_of_directed cc.directedOn fun x xc => hc xc
· exact fun _ => Set.subset_sUnion_of_mem
