dist_center_dist

Mathlib.Analysis.Complex.UpperHalfPlane.Metric

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.dist_center_dist

← MathLib Explorer

English

The distance from z to w.center(r) equals Im(w)·sinh(dist(z,w)).

Русский

Расстояние от z до w.center(r) равно Im(w)·sinh(dist(z,w)).

LaTeX

$$$\\operatorname{dist}(z, w.center(r)) = \\Im(w)\\sinh(\\operatorname{dist}(z,w)).$$$

Lean4

@[simp]
theorem dist_center_dist (z w : ℍ) : dist (z : ℂ) (w.center (dist z w)) = w.im * Real.sinh (dist z w) :=
  dist_eq_iff_dist_coe_center_eq.1 rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru