dist_eq_iff_dist_coe_center_eq — Mathlib

English

Distance equality: dist z w = r if and only if dist(z, w.center(r)) = Im(w)·sinh(r).

Русский

Расстояние между z и w равно r тогда и только тогда, когда dist(z, w.center(r)) = Im(w)·sinh(r).

LaTeX

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

Lean4

theorem dist_eq_iff_dist_coe_center_eq : dist z w = r ↔ dist (z : ℂ) (w.center r) = w.im * Real.sinh r :=
  eq_iff_eq_of_cmp_eq_cmp (cmp_dist_eq_cmp_dist_coe_center z w r)

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