lt_dist_iff_lt_dist_coe_center — Mathlib

English

Symmetric version of the previous comparison identity between hyperbolic and Euclidean distances after center translation.

Русский

Симметричная версия тождества сравнения между гиперболической и евклидовой дистанциями после перехода к центру.

LaTeX

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

Lean4

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

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