center — Mathlib

English

In the hyperbolic metric on the upper half-plane, the Euclidean center of the circle with center z and hyperbolic radius r has coordinates (Re z, Im z · cosh r).

Русский

В евклидовом представлении круг с центром z и гиперболическим радиусом r имеет центр (Re z, Im z · cosh r) в координатах Евклида.

LaTeX

$$$\\operatorname{center}(z,r) = (\\Re z, \\Im z \\cdot \\cosh r) \\quad (z \\in \\mathbb{H}).$$$

Lean4

/-- Euclidean center of the circle with center `z` and radius `r` in the hyperbolic metric. -/
def center (z : ℍ) (r : ℝ) : ℍ :=
  ⟨⟨z.re, z.im * Real.cosh r⟩, by positivity⟩

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