English
Let E be a normed inner product space over a field 𝕜. If {A} is a directed family of subspaces of E (ordered by inclusion) and each A in the family carries an orthonormal system when viewed as a subspace of E, then the union of all these subspaces forms an orthonormal family in E.
Русский
Пусть E — нормируемое внутриопределённое пространство над полем 𝕜. Пусть {A} — направленная семейство подпространств пространства E (по включению). Если каждое A в семействе содержит ортонормированную систему, считая элементы A как элементы E, то объединение ⋃A образует ортонормированную совокупность в E.
LaTeX
$$$\\operatorname{DirectedOn}(\\subseteq)\\ s \\wedge (\\forall a\\in s,\\ \\operatorname{Orthonormal}_{\\mathbb{K}}(\\lambda x: (x:a):E)) \\Rightarrow \\operatorname{Orthonormal}_{\\mathbb{K}}(\\lambda x: x: (\\bigcup_0 s)\\to E).$$$
Lean4
theorem orthonormal_sUnion_of_directed {s : Set (Set E)} (hs : DirectedOn (· ⊆ ·) s)
(h : ∀ a ∈ s, Orthonormal 𝕜 (fun x => ((x : a) : E))) : Orthonormal 𝕜 (fun x => x : ⋃₀ s → E) := by
rw [Set.sUnion_eq_iUnion]; exact orthonormal_iUnion_of_directed hs.directed_val (by simpa using h)
