dist_le_iff_le_sinh — Mathlib

English

The hyperbolic distance is bounded above by r iff a corresponding inequality involving sinh holds for half the distance.

Русский

Гиперболическое расстояние ограничено сверху значением r тогда и только тогда, когда выполняется соответствующее неравенство для sinh половины расстояния.

LaTeX

$$$dist(z,w) \le r \iff dist(z,w) / (2 \sqrt{z.im \cdot w.im}) \le \sinh(r/2)$$$

Lean4

theorem dist_le_iff_le_sinh : dist z w ≤ r ↔ dist (z : ℂ) w / (2 * √(z.im * w.im)) ≤ sinh (r / 2) := by
  rw [← div_le_div_iff_of_pos_right (zero_lt_two' ℝ), ← sinh_le_sinh, sinh_half_dist]

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