opNorm_lsmul_apply_le — Mathlib

English

For every scalar x in the ground field R, the left- multiplication operator by x on the normed space E has operator norm at most |x|, i.e., the induced linear map x ↦ (y ↦ x·y) has ‖·‖ ≤ ‖x‖.

Русский

Для каждого скаляра x из поля R оператор левого умножения на x на нормированном пространстве E имеет операторную норму не более |x|, то есть нормa индуцированного линейного отображения удовлетворяет ‖lsmul x‖ ≤ ‖x‖.

LaTeX

$$$\\|\\mathrm{lsmul}_{\\mathbb{K},R}(x) : E \\to_L[\\mathbb{K}]E\\| \\leq \\|x\\|$$$

Lean4

theorem opNorm_lsmul_apply_le (x : R) : ‖(lsmul 𝕜 R x : E →L[𝕜] E)‖ ≤ ‖x‖ :=
  ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg x) fun y => norm_smul_le x y

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