Theorems · Definition · functional analysis

continuousMultilinearCurryFin0

(𝕜 : Type u) →
  (G : Type wG) →
    (G' : Type wG') →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup G] →
          [inst_2 : NormedSpace 𝕜 G] →
            [inst_3 : NormedAddCommGroup G'] → [inst_4 : NormedSpace 𝕜 G'] → (G [×0]→L[𝕜] G') ≃ₗᵢ[𝕜] G'

The continuous linear isomorphism between elements of a normed space, and continuous multilinear maps in 0 variables with values in this normed space. The direct and inverse maps are uncurry0 and curry0. Use these unless you need the full framework of linear isometric equivs.

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Curry

Cited by

34 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace