nndist_self_conj

Mathlib.Analysis.Complex.Norm

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

English

The NN distance between z and its conjugate is the same as between z and its conjugate with nonnegative value, i.e., nndist(z, \overline{z}) = 2|Im z|.

Русский

NN-дистанция между z и сопряженным равна 2|Im z|.

LaTeX

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

Lean4

theorem nndist_self_conj (z : ℂ) : nndist z (conj z) = 2 * Real.nnabs z.im := by rw [nndist_comm, nndist_conj_self]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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