re_inner_le_norm — Mathlib

English

For any x, y in E, the real part of the inner product is bounded by the product of their norms: Re⟪x,y⟫ ≤ ∥x∥ ∥y∥.

Русский

Для любых x, y в E вещественная часть скалярного произведения ограничена произведением норм: Re⟪x,y⟫ ≤ ∥x∥ ∥y∥.

LaTeX

$$$\operatorname{Re}\langle x,y\rangle \le \|x\| \|y\|$$$

Lean4

theorem re_inner_le_norm (x y : E) : re ⟪x, y⟫ ≤ ‖x‖ * ‖y‖ :=
  le_trans (re_le_norm ⟪x, y⟫) (norm_inner_le_norm x y)

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