dist_coe_center — Mathlib

English

In the upper half-plane, the squared Euclidean distance between z and w.center(r) equals the same explicit expression in terms of Im parts and cosh/sinh of r and dist(z,w).

Русский

В верхней полуплоскости квадратичное евклидово расстояние между z и w.center(r) задаётся тем же явным выражением через мнимые части и cosh/sinh.

LaTeX

$$$\\operatorname{dist}(z, w.center(r))^2 = 2\\Im(z)\\Im(w)(\\cosh(\\operatorname{dist}(z,w)) - \\cosh r) + (\\Im(w)\\sinh r)^2.$$$

Lean4

theorem dist_coe_center (z w : ℍ) (r : ℝ) :
    dist (z : ℂ) (w.center r) = √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2) :=
  by rw [← sqrt_sq dist_nonneg, dist_coe_center_sq]

Похожие утверждения