dist_self_center — Mathlib

English

The distance from z to its center with radius r is Im(z)·(cosh r − 1).

Русский

Расстояние от z до центра z с радиусом r равно Im(z)·(cosh r − 1).

LaTeX

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

Lean4

@[simp]
theorem dist_self_center (z : ℍ) (r : ℝ) : dist (z : ℂ) (z.center r) = z.im * (Real.cosh r - 1) :=
  by
  rw [dist_of_re_eq (z.center_re r).symm, dist_comm, Real.dist_eq, mul_sub, mul_one]
  exact abs_of_nonneg (sub_nonneg.2 <| le_mul_of_one_le_right z.im_pos.le (one_le_cosh _))

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