Theorems · Definition · functional analysis

Pi.orthonormalBasis

{η : Type u_7} →
  [inst : Fintype η] →
    {ι : η → Type u_8} →
      [inst_1 : (i : η) → Fintype (ι i)] →
        {𝕜 : Type u_9} →
          [inst_2 : RCLike 𝕜] →
            {E : η → Type u_10} →
              [inst_3 : (i : η) → NormedAddCommGroup (E i)] →
                [inst_4 : (i : η) → InnerProductSpace 𝕜 (E i)] →
                  ((i : η) → OrthonormalBasis (ι i) 𝕜 (E i)) → OrthonormalBasis ((i : η) × ι i) 𝕜 (PiLp 2 E)

Pi.orthonormalBasis (B : ∀ i, OrthonormalBasis (ι i) 𝕜 (E i)) is the Σ i, ι i-indexed orthonormal basis on Π i, E i given by B i on each component.

Defined in

Mathlib.Analysis.InnerProductSpace.PiL2

Cited by

3 results in Mathlib

Foundations

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

Assumes

FintypeFintypeRCLikeNormedAddCommGroupInnerProductSpace