auxbound2 — Mathlib

English

For c ∈ ℝ and d ∈ ℝ with 1 ≤ d^2, we have r(z) ≤ |c z + d|.

Русский

Для c ∈ ℝ и d ∈ ℝ с условием 1 ≤ d^2 выполняется r(z) ≤ |c z + d|.

LaTeX

$$$\\forall z \\in \\mathbb{H},\\; \\forall c \\in \\mathbb{R},\\; 1 \\le d^2 \\Rightarrow r(z) \\le \\| c z + d \\|$$$

Lean4

theorem auxbound2 (c : ℝ) {d : ℝ} (hd : 1 ≤ d ^ 2) : r z ≤ ‖c * (z : ℂ) + d‖ :=
  by
  have H1 : √(r1 z) ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2) :=
    (Real.sqrt_le_sqrt_iff (by positivity)).mpr (r1_aux_bound _ _ hd)
  simpa only [r, norm_def, normSq_apply, add_re, re_ofReal_mul, coe_re, ofReal_re, ← pow_two, add_im, im_ofReal_mul,
    coe_im, ofReal_im, add_zero, min_le_iff] using Or.inr H1

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