Theorems · Definition · functional analysis

DirectSum.IsInternal.collectedOrthonormalBasis

{ι : Type u_1} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : Fintype ι] →
              {A : ι → Submodule 𝕜 E} →
                (OrthogonalFamily 𝕜 (fun i => ↥(A i)) fun i => (A i).subtypeₗᵢ) →
                  [inst_4 : DecidableEq ι] →
                    (DirectSum.IsInternal fun i => A i) →
                      {α : ι → Type u_7} →
                        [inst_5 : (i : ι) → Fintype (α i)] →
                          ((i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)) → OrthonormalBasis ((i : ι) × α i) 𝕜 E

Given an internal direct sum decomposition of a module M, and an orthonormal basis for each of the components of the direct sum, the disjoint union of these orthonormal bases is an orthonormal basis for M.

Defined in

Mathlib.Analysis.InnerProductSpace.PiL2

Cited by

5 results in Mathlib

Foundations

Depth 232 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFintypeDecidableEqFintype