Theorems · Theorem · functional analysis

ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const

∀ {𝕜 : Type u} {n : ℕ} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] {k l : ℕ} {s : Finset (Fin n)}
  (hk : s.card = k) (hl : sᶜ.card = l) (f : G [×k]→L[𝕜] G [×l]→L[𝕜] G') (x y : G),
  ((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl).symm f) (s.piecewise (fun x_1 => x) fun x => y) =
    (f fun x_1 => x) fun x => y

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Curry

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace