Theorems · Definition · functional analysis

ContinuousLinearMap.uncurryLeft

{𝕜 : 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] → (Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G) → ContinuousMultilinearMap 𝕜 Ei G

Given a continuous linear map f from E 0 to continuous multilinear maps on n variables, construct the corresponding continuous multilinear map on n+1 variables obtained by concatenating the variables, given by m ↦ f (m 0) (tail m)

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Curry

Cited by

7 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace