norm_le — Mathlib

English

Similarly, the norm of the imaginary part is not larger than the norm of x.

Русский

Аналогично, норма мнимой части не превосходит норму x.

LaTeX

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

Lean4

theorem norm_le (x : A) : ‖imaginaryPart x‖ ≤ ‖x‖ := by
  calc
    ‖imaginaryPart x‖ = ‖realPart (Complex.I • (-x))‖ := by simp
    _ ≤ ‖x‖ := by
      simpa only [smul_neg, map_neg, realPart_I_smul, neg_neg, AddSubgroupClass.coe_norm, norm_neg, norm_smul,
        Complex.norm_I, one_mul] using realPart.norm_le (Complex.I • (-x))

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