im_div_exp_dist_le — Mathlib

English

The distance to the center can be written via cosh and sinh-related identities; it matches the earlier center-distance formula.

Русский

Расстояние до центра записывается через тождества, связанные с cosh и sinh; совпадает с ранее установленной формулой для центра и расстояния.

LaTeX

$$$\\operatorname{dist}(z, \\operatorname{center}(z,r)) = \\Im(z) (\\cosh r - 1).$$$

Lean4

theorem im_div_exp_dist_le (z w : ℍ) : z.im / Real.exp (dist z w) ≤ w.im :=
  (div_le_iff₀ (exp_pos _)).2 (im_le_im_mul_exp_dist z w)

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