conj — Mathlib

English

Conjugation on the unit disc is the natural involution induced by complex conjugation; applying it twice yields the original point.

Русский

Сопряжение на единичном диске — это естественная инволюция, получаемая взятием комплексного сопряжения; дважды применённое возвращает исходную точку.

LaTeX

$$$\forall z \in \mathbb{D}, \operatorname{conj}(z) \in \mathbb{D} \land \operatorname{conj}(\operatorname{conj}(z)) = z$$$

Lean4

/-- Conjugate point of the unit disc. -/
def conj (z : 𝔻) : 𝔻 :=
  mk (conj' ↑z) <| (norm_conj z).symm ▸ z.norm_lt_one

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