normSq_le_normSq_of_re_le_of_im_le

English

If |x.re| ≤ |y.re| and |x.im| ≤ |y.im| then normSq x ≤ normSq y.

Русский

Если |x.re| ≤ |y.re| и |x.im| ≤ |y.im|, то нормaSq x ≤ normSq y.

LaTeX

$$$ |x.re| \le |y.re| \wedge |x.im| \le |y.im| \Rightarrow \operatorname{normSq}(x) \le \operatorname{normSq}(y) $$$

Lean4

theorem normSq_le_normSq_of_re_le_of_im_le {x y : ℂ} (hre : |x.re| ≤ |y.re|) (him : |x.im| ≤ |y.im|) :
    Complex.normSq x ≤ Complex.normSq y :=
  by
  rw [normSq_apply, normSq_apply, ← _root_.abs_mul_self, _root_.abs_mul, ← _root_.abs_mul_self y.re,
    _root_.abs_mul y.re, ← _root_.abs_mul_self x.im, _root_.abs_mul x.im, ← _root_.abs_mul_self y.im,
    _root_.abs_mul y.im]
  gcongr

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