auxbound1 — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem auxbound1 {c : ℝ} (d : ℝ) (hc : 1 ≤ c ^ 2) : r z ≤ ‖c * (z : ℂ) + d‖ :=
  by
  rcases z with ⟨z, hz⟩
  have H1 : z.im ≤ √((c * z.re + d) ^ 2 + (c * z).im ^ 2) :=
    by
    rw [Real.le_sqrt' hz, im_ofReal_mul, mul_pow]
    exact (le_mul_of_one_le_left (sq_nonneg _) hc).trans <| le_add_of_nonneg_left (sq_nonneg _)
  simpa only [r, norm_def, normSq_apply, add_re, re_ofReal_mul, coe_re, ← pow_two, add_im, mul_im, coe_im, ofReal_im,
    zero_mul, add_zero, min_le_iff] using Or.inl H1

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