Theorems · Theorem · functional analysis

ContinuousMultilinearMap.norm_map_snoc_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 : ContinuousMultilinearMap 𝕜 Ei G)
  (m : (i : Fin n) → Ei i.castSucc) (x : Ei (Fin.last n)), ‖f (Fin.snoc m x)‖ ≤ (‖f‖ * ∏ i, ‖m i‖) * ‖x‖

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Curry

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace