dist_self_conj — Mathlib

English

The distance between z and its conjugate is the same as between z and its conjugate (commutativity): dist(z, \overline{z}) = dist(\overline{z}, z) = 2|Im z|.

Русский

Расстояние между z и сопряженным равно расстоянию между сопряженным и z: dist(z, \overline{z}) = dist(\overline{z}, z) = 2|Im z|.

LaTeX

$$$\\\\operatorname{dist}(z, \\overline{z}) = 2 \\, |\\\\operatorname{Im} z|$$$

Lean4

theorem dist_self_conj (z : ℂ) : dist z (conj z) = 2 * |z.im| := by rw [dist_comm, dist_conj_self]

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