dist_conj_comm

Mathlib.Analysis.Complex.Basic

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

English

For all z, w ∈ ℂ, dist(conj z, w) = dist(z, conj w).

Русский

Для любых z, w ∈ ℂ выполняется равенство d(\overline{z}, w) = d(z, \overline{w}).

LaTeX

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

Lean4

theorem dist_conj_comm (z w : ℂ) : dist (conj z) w = dist z (conj w) := by rw [← dist_conj_conj, conj_conj]

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

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

Разделы

Аффилиация

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