Theorems · Theorem · functional analysis

ContinuousMultilinearMap.norm_map_init_le

∀ {𝕜 : 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 i.castSucc [×n]→L[𝕜] Ei (Fin.last n) →L[𝕜] G)
  (m : (i : Fin n.succ) → Ei i), ‖(f (Fin.init m)) (m (Fin.last n))‖ ≤ ‖f‖ * ∏ i, ‖m i‖

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Curry

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace