norm_le — Mathlib

English

For any x in a normed space with a complex structure, the norm of its real part is at most the norm of x.

Русский

Для любого x в нормированном пространстве с комплексной структурой норма вещественной части не превосходит нормы самого x.

LaTeX

$$\\|\\operatorname{realPart}(x)\\| \\leq \\|x\\|$$

Lean4

theorem norm_le (x : A) : ‖realPart x‖ ≤ ‖x‖ :=
  by
  rw [← inv_mul_cancel_left₀ two_ne_zero ‖x‖, ← AddSubgroup.norm_coe, realPart_apply_coe, norm_smul, norm_inv,
    Real.norm_ofNat]
  gcongr
  exact norm_add_le _ _ |>.trans <| by simp [two_mul]

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