Theorems · Definition · functional analysis

ContinuousMultilinearMap.uncurry0

(𝕜 : 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' → G [×0]→L[𝕜] G'

Associating to an element x of a vector space E₂ the continuous multilinear map in 0 variables taking the (unique) value x

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Curry

Cited by

28 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace