center_im

Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

English

The imaginary part of the center of z is Im(z) · cosh r.

Русский

Воображаемая часть центра равна Im(z) · cosh r.

LaTeX

$$$\\operatorname{center}(z,r)_{\\Im} = \\Im(z) \\cdot \\cosh r.$$$

Lean4

@[simp]
theorem center_im (z r) : (center z r).im = z.im * Real.cosh r :=
  rfl

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

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

Разделы

Аффилиация

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