English
Let z be a point of the upper half-plane and r a real radius. Under the natural inclusion i: ℍ → ℂ, the image of the ball in ℍ centered at z with radius r is the Euclidean ball in ℂ centered at z.center(r) with radius z.im · sinh(r).
Русский
Пусть z принадлежит верхней полуплоскости и r — вещественный радиус. Под естественным вложением i: ℍ → ℂ образ шара Bℍ(z,r) равен евклидову шару в ℂ с центром в z.center(r) и радиусом z.im · sinh(r).
LaTeX
$$$$ i\\big(\\mathrm{ball}_{\\mathbb{H}}(z,r)\\big) = \\mathrm{ball}_{\\mathbb{C}}\\big( z.center(r),\\ z.im \\cdot \\sinh r\\big). $$$$
Lean4
theorem image_coe_ball (z : ℍ) (r : ℝ) : ((↑) : ℍ → ℂ) '' ball (α := ℍ) z r = ball ↑(z.center r) (z.im * Real.sinh r) :=
by
ext w; constructor
· rintro ⟨w, hw, rfl⟩
exact dist_lt_iff_dist_coe_center_lt.1 hw
· intro hw
lift w to ℍ using im_pos_of_dist_center_le (ball_subset_closedBall hw)
exact mem_image_of_mem _ (dist_lt_iff_dist_coe_center_lt.2 hw)
