edist_of_re_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem edist_of_re_eq {z w : ℂ} (h : z.re = w.re) : edist z w = edist z.im w.im := by
  rw [edist_nndist, edist_nndist, nndist_of_re_eq h]

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