orthonormal_span — Mathlib

English

If v_family is orthonormal, then the sigma-extended family given by V on the associated sum is orthonormal as well.

Русский

Если v_family ортонормирован, то сумма через σ-образование даёт также ортонормированную систему.

LaTeX

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

Lean4

theorem orthonormal_span {ι : Type*} {v : ι → E} (hv : Orthonormal 𝕜 v) :
    @Orthonormal 𝕜 (Submodule.span 𝕜 (Set.range v)) _ _ _ ι fun i : ι =>
      ⟨v i, Submodule.subset_span (Set.mem_range_self i)⟩ :=
  hv.codRestrict (Submodule.span 𝕜 (Set.range v)) fun i => Submodule.subset_span (Set.mem_range_self i)

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