instSeminormedAddCommGroup — Mathlib

English

For any f in ContinuousMultilinearMap 𝕜 E F and x in the tensor, the operator norm of lift f applied to x is bounded by the product of the operator norm of f and the injective seminorm of x.

Русский

Для любого f ∈ ContinuousMultilinearMap и x в тензоре, Norm( lift f )(x ) ≤ ‖f‖ · ‖x‖_{inj}.

LaTeX

$$$\\|\\mathrm{lift}(f)(x)\\| ≤ \\|f\\| \\cdot \\|x\\|_{inj}$$$

Lean4

noncomputable instance : SeminormedAddCommGroup (⨂[𝕜] i, E i) :=
  AddGroupSeminorm.toSeminormedAddCommGroup injectiveSeminorm.toAddGroupSeminorm

Похожие утверждения