isometry_vertical_line — Mathlib

English

For every real a, the map y ↦ a + i e^{y} defines an isometry from ℝ into ℍ with respect to the hyperbolic metric.

Русский

Для каждого вещественного a отображение y ↦ a + i e^{y} задаёт изометрию от ℝ в ℍ относительно гиперболической метрики.

LaTeX

$$$$ \\text{For all } a \\in \\mathbb{R},\\ \\; y \\mapsto a + i e^{y} \\text{ is an isometry } \\mathbb{R} \\to \\mathbb{H}. $$$$

Lean4

theorem isometry_vertical_line (a : ℝ) : Isometry fun y => mk ⟨a, exp y⟩ (exp_pos y) :=
  by
  refine Isometry.of_dist_eq fun y₁ y₂ => ?_
  rw [dist_of_re_eq]
  exacts [congr_arg₂ _ (log_exp _) (log_exp _), rfl]

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