English
The image of a closed Euclidean ball under the embedding of the upper half-plane into the complex plane is itself a closed Euclidean ball centered at the center with radius Im(z)·sinh r.
Русский
Образ замкнутого евклидова шара при вложении верхней полуплоскости в комплексную плоскость есть замкнутый евклидовый шар, центр которого имеет координаты center(z,r) и радиус Im(z)·sinh r.
LaTeX
$$$\\bigl(\\mathbb{H} \\hookrightarrow \\mathbb{C}\\bigr)\\,'\\mathrm{image}(\\operatorname{closedBall}(z,r)) = \\operatorname{closedBall}(\\operatorname{center}(z,r), \\Im(z)\\sinh r).$$$
Lean4
/-- An upper estimate on the complex distance between two points in terms of the hyperbolic distance
and the imaginary part of one of the points. -/
theorem le_dist_coe (z w : ℍ) : w.im * (1 - Real.exp (-dist z w)) ≤ dist (z : ℂ) w :=
calc
w.im * (1 - Real.exp (-dist z w)) = dist (z : ℂ) (w.center (dist z w)) - dist (w : ℂ) (w.center (dist z w)) := by
rw [dist_center_dist, dist_self_center, ← Real.cosh_sub_sinh]; ring
_ ≤ dist (z : ℂ) w := sub_le_iff_le_add.2 <| dist_triangle _ _ _
