nndist_of_re_eq — Mathlib

English

If Re(z) = Re(w), then the nonnegative distance between z and w equals the nonnegative distance between their imaginary parts: nndist(z, w) = nndist(Im z, Im w).

Русский

Если Re(z) = Re(w), то NN-дистанция между z и w равна NN-дистанции между их мнимыми частями: nndist(z, w) = nndist(Im z, Im w).

LaTeX

$$$\\\\mathrm{nndist}(z,w) = nndist(\\\\operatorname{Im} z, \\\\operatorname{Im} w)$$$

Lean4

theorem nndist_of_re_eq {z w : ℂ} (h : z.re = w.re) : nndist z w = nndist z.im w.im :=
  NNReal.eq <| dist_of_re_eq h

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