English
The image of closedBall under the complex embedding equals closedBall with the center scaled by no more than the hyperbolic radius, matching the same center-radius relation as before.
Русский
Образ замкнутого шара под отображением в комплексную плоскость равен замкнутому шару с центром, масштабированным в соответствии с радиусом гиперболической метрики.
LaTeX
$$$\\text{image}_{\\mathbb{C}}(\\overline{B}_{\\mathbb{H}}(z,r)) = \\overline{B}_{\\mathbb{C}}(\\operatorname{center}(z,r).\\mathrm{coe}, \\Im(z)\\sinh r).$$$
Lean4
theorem image_coe_closedBall (z : ℍ) (r : ℝ) :
((↑) : ℍ → ℂ) '' closedBall (α := ℍ) z r = closedBall ↑(z.center r) (z.im * Real.sinh r) :=
by
ext w; constructor
· rintro ⟨w, hw, rfl⟩
exact dist_le_iff_dist_coe_center_le.1 hw
· intro hw
lift w to ℍ using im_pos_of_dist_center_le hw
exact mem_image_of_mem _ (dist_le_iff_dist_coe_center_le.2 hw)
