English
Repeat: directed union of orthonormal subfamilies remains orthonormal.
Русский
Повтор: направленное объединение ортонормированных подпоследовательностей остаётся ортонормированным.
LaTeX
$$$\operatorname{Orthonormal} 𝕜 (\bigcup_i s_i) \text{ with directed inclusion} $$$
Lean4
theorem orthonormal_iUnion_of_directed {η : Type*} {s : η → Set E} (hs : Directed (· ⊆ ·) s)
(h : ∀ i, Orthonormal 𝕜 (fun x => x : s i → E)) : Orthonormal 𝕜 (fun x => x : (⋃ i, s i) → E) := by
classical
rw [orthonormal_subtype_iff_ite]
rintro x ⟨_, ⟨i, rfl⟩, hxi⟩ y ⟨_, ⟨j, rfl⟩, hyj⟩
obtain ⟨k, hik, hjk⟩ := hs i j
have h_orth : Orthonormal 𝕜 (fun x => x : s k → E) := h k
rw [orthonormal_subtype_iff_ite] at h_orth
exact h_orth x (hik hxi) y (hjk hyj)