Theorems · Definition · functional analysis

LinearIsometryEquiv.piLpCurry

(𝕜 : Type u_1) →
  [inst : Semiring 𝕜] →
    {ι : Type u_5} →
      {κ : ι → Type u_6} →
        (p : ENNReal) →
          [inst_1 : Fact (1 ≤ p)] →
            [inst_2 : Fintype ι] →
              [inst_3 : (i : ι) → Fintype (κ i)] →
                (α : (i : ι) → κ i → Type u_7) →
                  [inst_4 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)] →
                    [inst_5 : (i : ι) → (k : κ i) → Module 𝕜 (α i k)] →
                      (PiLp p fun i => α i.fst i.snd) ≃ₗᵢ[𝕜] PiLp p fun i => PiLp p (α i)

LinearEquiv.piCurry for PiLp, as an isometry.

Defined in

Mathlib.Analysis.Normed.Lp.PiLp

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringFactFintypeFintypeSeminormedAddCommGroupModule