Theorems · Definition · functional analysis

continuousMultilinearCurryRightEquiv

(𝕜 : 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 i.castSucc [×n]→L[𝕜] Ei (Fin.last n) →L[𝕜] G

The space of continuous multilinear maps on Π(i : Fin (n+1)), Ei i is canonically isomorphic to the space of continuous multilinear maps on Π(i : Fin n), Ei <| castSucc i with values in the space of continuous linear maps on Ei (last n), by separating the last variable. We register this isomorphism as a continuous linear equiv in continuousMultilinearCurryRightEquiv 𝕜 Ei G. The algebraic version (without topology) is given in multilinearCurryRightEquiv 𝕜 Ei G. The direct and inverse maps are given by f.curryRight and f.uncurryRight. Use these unless you need the full framework of linear isometric equivs.

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Curry

Cited by

4 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace