le_dist_iff_le_dist_coe_center

Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem le_dist_iff_le_dist_coe_center : r < dist z w ↔ w.im * Real.sinh r < dist (z : ℂ) (w.center r) :=
  lt_iff_lt_of_cmp_eq_cmp (cmp_eq_cmp_symm.1 <| cmp_dist_eq_cmp_dist_coe_center z w r)

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

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

Разделы

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

Аффилиация

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