cosh_dist' — Mathlib

English

For points z and w in the upper half-plane, the hyperbolic distance dist(z,w) satisfies an explicit cosh formula in terms of their real and imaginary parts.

Русский

Для точек z,w на полуплоскости верхней гиперболической дистанции выполняется явная формула для cosh( dist(z,w) ) через их вещественную и мнимую части.

LaTeX

$$$\\cosh(\\operatorname{dist}(z,w)) = \\frac{(\\Re z - \\Re w)^2 + (\\Im z)^2 + (\\Im w)^2}{2\\, \\Im z \\Im w}, \\quad z,w \\in \\mathbb{H}$$$

Lean4

theorem cosh_dist' (z w : ℍ) : Real.cosh (dist z w) = ((z.re - w.re) ^ 2 + z.im ^ 2 + w.im ^ 2) / (2 * z.im * w.im) :=
  by
  simp [field, cosh_dist, Complex.dist_eq, Complex.sq_norm, normSq_apply]
  ring

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