center_re

Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

English

The real part of the center of z is preserved: Re(center(z,r)) = Re(z).

Русский

Действительная часть центра сохраняется: Re(center(z,r)) = Re(z).

LaTeX

$$$\\operatorname{center}(z,r)_{\\Re} = \\Re(z).$$$

Lean4

@[simp]
theorem center_re (z r) : (center z r).re = z.re :=
  rfl

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

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

Разделы

Аффилиация

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