Theorems · Definition · functional analysis

PiLp.sumPiLpEquivProdLpPiLp

{𝕜 : Type u_1} →
  [inst : Semiring 𝕜] →
    {ι : Type u_5} →
      {κ : Type u_6} →
        (p : ENNReal) →
          (α : ι ⊕ κ → Type u_7) →
            [inst_1 : Fintype ι] →
              [inst_2 : Fintype κ] →
                [inst_3 : Fact (1 ≤ p)] →
                  [inst_4 : (i : ι ⊕ κ) → SeminormedAddCommGroup (α i)] →
                    [inst_5 : (i : ι ⊕ κ) → Module 𝕜 (α i)] →
                      WithLp p ((i : ι ⊕ κ) → α i) ≃ₗᵢ[𝕜]
                        WithLp p (WithLp p ((i : ι) → α (Sum.inl i)) × WithLp p ((i : κ) → α (Sum.inr i)))

LinearEquiv.sumPiEquivProdPi for PiLp, as an isometry.

Defined in

Mathlib.Analysis.Normed.Lp.PiLp

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringFintypeFintypeFactSeminormedAddCommGroupModule