Theorems · Theorem · functional analysis

ContinuousMultilinearMap.curryFinFinset_apply_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 [×n]→L[𝕜] G') (x y : G),
  ((((ContinuousMultilinearMap.curryFinFinset 𝕜 G G' hk hl) f) fun x_1 => x) fun x => y) =
    f (s.piecewise (fun x_1 => x) fun x => y)

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Curry

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace