nndist_conj_self

Mathlib.Analysis.Complex.Norm

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

← MathLib Explorer

English

For z = a + bi, the NN distance between z and its conjugate is nndist(z, \overline{z}) = 2|b|.

Русский

Для z = a + bi NN-дистанция между z и \overline{z} равна 2|b|.

LaTeX

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

Lean4

theorem nndist_conj_self (z : ℂ) : nndist (conj z) z = 2 * Real.nnabs z.im :=
  NNReal.eq <| by rw [← dist_nndist, NNReal.coe_mul, NNReal.coe_two, Real.coe_nnabs, dist_conj_self]

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

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

Разделы

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

Аффилиация

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