dist_lt_iff_dist_coe_center_lt — Mathlib

English

The comparison of distances (using a comparison function cmp) between z,w and their center translates exactly through cosh/sinh expressions.

Русский

Сравнение расстояний через функцию сравнения совпадает между гиперболической и евклидовой точкой через cosh/sinh.

LaTeX

$$$\\text{cmp}(\\operatorname{dist}(z,w), r) = \\text{cmp}(\\operatorname{dist}(z,w.center(r)), \\Im(w)\\sinh r).$$$

Lean4

theorem dist_lt_iff_dist_coe_center_lt : dist z w < r ↔ dist (z : ℂ) (w.center r) < w.im * Real.sinh r :=
  lt_iff_lt_of_cmp_eq_cmp (cmp_dist_eq_cmp_dist_coe_center z w r)

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