dist_eq_iff_eq_sinh — Mathlib

English

For any z,w in the upper half-plane and any real r, dist(z,w) = r iff dist(z,w) expressed in the complex metric equals sinh(r/2).

Русский

Для любых z,w в верхней полуплоскости и любого вещественного r, dist(z,w) = r тогда и только тогда, что выражение в метерике ℂ равно sinh(r/2).

LaTeX

$$$dist(z,w) = r \iff dist(z,w)_{\mathbb{C}} / (2 \sqrt{z.im w.im}) = \sinh(r/2)$$$

Lean4

theorem dist_eq_iff_eq_sinh : dist z w = r ↔ dist (z : ℂ) w / (2 * √(z.im * w.im)) = sinh (r / 2) := by
  rw [← div_left_inj' (two_ne_zero' ℝ), ← sinh_inj, sinh_half_dist]

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