Theorems · Theorem · functional analysis

ContinuousLinearMap.curry_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] (f : Ei 0 →L[𝕜] Ei i.succ [×n]→L[𝕜] G),
  f.uncurryLeft.curryLeft = f

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Curry

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace