orthonormal_iUnion_of_directed — Mathlib

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)

Похожие утверждения