opNorm_lsmul_le — Mathlib

English

The operator norm of the map that sends x to the left-multiplication by x, viewed as a bounded linear map from R to the space of bounded linear operators on E, is at most 1.

Русский

Норма оператора, сопоставляющего x слева на умножение, не превосходит единицы.

LaTeX

$$$\\|\\mathrm{lsmul}_{\\mathbb{K},R}\\| \\leq 1$$$

Lean4

/-- The norm of `lsmul` is at most 1 in any semi-normed group. -/
theorem opNorm_lsmul_le : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ ≤ 1 :=
  by
  refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun x => ?_
  simp_rw [one_mul]
  exact opNorm_lsmul_apply_le _

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