dist_log_im_le — Mathlib

English

The hyperbolic distance between z and w dominates the distance between log z.im and log w.im.

Русский

Гиперболическая дистанция между z и w доминирует над расстоянием между log(z.im) и log(w.im).

LaTeX

$$$\\operatorname{dist}(\\log z.im, \\log w.im) \\le \\operatorname{dist}(z,w).$$$

Lean4

/-- Hyperbolic distance between two points is greater than or equal to the distance between the
logarithms of their imaginary parts. -/
theorem dist_log_im_le (z w : ℍ) : dist (log z.im) (log w.im) ≤ dist z w :=
  calc
    dist (log z.im) (log w.im) = dist (mk ⟨0, z.im⟩ z.im_pos) (mk ⟨0, w.im⟩ w.im_pos) := Eq.symm <| dist_of_re_eq rfl
    _ ≤ dist z w := by
      simp_rw [dist_eq]
      dsimp only [coe_mk, mk_im]
      gcongr
      simpa [sqrt_sq_eq_abs] using Complex.abs_im_le_norm (z - w)

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