dist_of_re_eq — Mathlib

English

Let z, w be complex numbers with equal real parts, then the distance between z and w equals the distance between their imaginary parts: dist(z, w) = dist(Im z, Im w).

Русский

Пусть z, w ∈ ℂ и z.re = w.re. Тогда расстояние между z и w равно расстоянию между их мнимыми частями: dist(z, w) = dist(Im z, Im w).

LaTeX

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

Lean4

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

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