Theorems · Definition · functional analysis

continuousMultilinearCurryLeftEquiv

(𝕜 : Type u) →
  {n : ℕ} →
    (Ei : Fin n.succ → Type wEi) →
      (G : Type wG) →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] →
            [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)] →
              [inst_3 : NormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] → ContinuousMultilinearMap 𝕜 Ei G ≃ₗᵢ[𝕜] Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G

The space of continuous multilinear maps on Π(i : Fin (n+1)), E i is canonically isomorphic to the space of continuous linear maps from E 0 to the space of continuous multilinear maps on Π(i : Fin n), E i.succ, by separating the first variable. We register this isomorphism in continuousMultilinearCurryLeftEquiv 𝕜 E E₂. The algebraic version (without topology) is given in multilinearCurryLeftEquiv 𝕜 E E₂. The direct and inverse maps are given by f.curryLeft and f.uncurryLeft. Use these unless you need the full framework of linear isometric equivs.

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Curry

Cited by

32 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace