orthonormal_sigma_orthonormal — Mathlib

English

If each v_family i is an orthonormal basis, then the combined family given by the sigma construction is orthonormal.

Русский

Если каждый v_family i образует ортонормальный базис, то совокупность, образованная по конструированию через сигму, ортонормальна.

LaTeX

$$Orthonormal 𝕜 fun a => V a.1 (v_family a.1 a.2)$$

Lean4

theorem orthonormal_sigma_orthonormal {α : ι → Type*} {v_family : ∀ i, α i → G i}
    (hv_family : ∀ i, Orthonormal 𝕜 (v_family i)) : Orthonormal 𝕜 fun a : Σ i, α i => V a.1 (v_family a.1 a.2) :=
  by
  constructor
  · rintro ⟨i, v⟩
    simpa only [LinearIsometry.norm_map] using (hv_family i).left v
  rintro ⟨i, v⟩ ⟨j, w⟩ hvw
  by_cases hij : i = j
  · subst hij
    have : v ≠ w := fun h => by
      subst h
      exact hvw rfl
    simpa only [LinearIsometry.inner_map_map] using (hv_family i).2 this
  · exact hV hij (v_family i v) (v_family j w)

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