dist_of_im_eq — Mathlib

English

If Im(z) = Im(w), then the distance dist(z,w) equals the distance between their real parts: dist(z,w) = dist(Re z, Re w).

Русский

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

LaTeX

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

Lean4

theorem dist_of_im_eq {z w : ℂ} (h : z.im = w.im) : dist z w = dist z.re w.re := by
  rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]

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