Theorems · Theorem · functional analysis

PiTensorProduct.norm_eval_le_projectiveSeminorm

∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {G : Type u_4}
  [inst_4 : SeminormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G)
  (x : PiTensorProduct 𝕜 fun i => E i), ‖(PiTensorProduct.lift f.toMultilinearMap) x‖ ≤ ‖f‖ * ‖x‖

Defined in

Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeSeminormedAddCommGroupNontriviallyNormedFieldNormedSpaceSeminormedAddCommGroupNormedSpace