re

Mathlib.Analysis.Complex.UnitDisc.Basic

URI: https://scilib.ai/kg/mathlib#Complex.UnitDisc.re

English

The real part of a point of the unit disk is the real part of its complex value.

Русский

Действительная часть точки единичного диска равна действительной части её комплексного значения.

LaTeX

$$$ re(z) = \\Re(z) \\quad \\text{for } z \\in 𝔻 $$$

Lean4

/-- Real part of a point of the unit disc. -/
def re (z : 𝔻) : ℝ :=
  Complex.re z

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

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

Разделы

Аффилиация

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