English
Let z ∈ ℍ and r ∈ ℝ. The image of the sphere in ℍ with center z and radius r under the standard inclusion into ℂ is the sphere in ℂ with center z.center(r) and radius z.im · sinh r.
Русский
Пусть z ∈ ℍ и r ∈ ℝ. Образ сферы sphereℍ(z,r) под естественным вложением в ℂ есть сфера в ℂ с центром z.center(r) и радиусом z.im · sinh r.
LaTeX
$$$$ i\\big(\\mathrm{sphere}_{\\mathbb{H}}(z,r)\\big) = \\mathrm{sphere}_{\\mathbb{C}}\\big( z.center(r),\\ z.im \\cdot \\sinh r\\big). $$$$
Lean4
theorem image_coe_sphere (z : ℍ) (r : ℝ) :
((↑) : ℍ → ℂ) '' sphere (α := ℍ) z r = sphere ↑(z.center r) (z.im * Real.sinh r) :=
by
ext w; constructor
· rintro ⟨w, hw, rfl⟩
exact dist_eq_iff_dist_coe_center_eq.1 hw
· intro hw
lift w to ℍ using im_pos_of_dist_center_le (sphere_subset_closedBall hw)
exact mem_image_of_mem _ (dist_eq_iff_dist_coe_center_eq.2 hw)
