edist_of_im_eq — Mathlib

English

If Im(z) = Im(w), then edist(z,w) = edist(Re z, Re w).

Русский

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

LaTeX

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

Lean4

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

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