nnnorm_inner_le_nnnorm — Mathlib

English

For all x, y in E, the nnnorm of their inner product is bounded by the product of their nnnorms: ‖⟪x,y⟫‖₊ ≤ ‖x‖₊ · ‖y‖₊.

Русский

Для любых x, y в E nn-норма скалярного произведения удовлетворяет неравенству: ‖⟪x,y⟫‖₊ ≤ ‖x‖₊ · ‖y ₊.

LaTeX

$$$\|\langle x,y\rangle\|_+ \le \|x\|_+ \|y\|_+$$$

Lean4

theorem nnnorm_inner_le_nnnorm (x y : E) : ‖⟪x, y⟫‖₊ ≤ ‖x‖₊ * ‖y‖₊ :=
  norm_inner_le_norm x y

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