English
An upper bound on the complex distance between z and w is given by a function of the distance in the hyperbolic metric and the imaginary part of w.
Русский
Граница расстояния в комплексной плоскости задаётся функцией от гиперболического расстояния и мнимой части w.
LaTeX
$$$\\operatorname{dist}_{\\mathbb{C}}(z,w) \\le \\Im(w)\\bigl(e^{\\operatorname{dist}(z,w)} - 1\\bigr).$$$
Lean4
theorem im_pos_of_dist_center_le {z : ℍ} {r : ℝ} {w : ℂ} (h : dist w (center z r) ≤ z.im * Real.sinh r) : 0 < w.im :=
calc
0 < z.im * (Real.cosh r - Real.sinh r) := mul_pos z.im_pos (sub_pos.2 <| sinh_lt_cosh _)
_ = (z.center r).im - z.im * Real.sinh r := (mul_sub _ _ _)
_ ≤ (z.center r).im - dist (z.center r : ℂ) w := (sub_le_sub_left (by rwa [dist_comm]) _)
_ ≤ w.im := sub_le_comm.1 <| (le_abs_self _).trans (abs_im_le_norm <| z.center r - w)
