isometry_conj

Mathlib.Analysis.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.isometry_conj

English

Conjugation is an isometry: dist(conj z, conj w) = dist(z, w).

Русский

Сопряжение сохраняет расстояние: dist(conj z, conj w) = dist(z, w).

LaTeX

$$$$ \\operatorname{dist}(\\overline{z}, \\overline{w}) = \\operatorname{dist}(z,w). $$$$

Lean4

theorem isometry_conj : Isometry (conj : ℂ → ℂ) :=
  conjLIE.isometry

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

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

Разделы

Аффилиация

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