dist_eq_re_im — Mathlib

English

The distance between z and w equals the square root of the sum of squares of the differences of real and imaginary parts: dist(z,w) = sqrt((Re z - Re w)^2 + (Im z - Im w)^2).

Русский

Расстояние между z и w равно корню из суммы квадратов разностей действительных и мнимых частей: dist(z,w) = sqrt((Re z - Re w)^2 + (Im z - Im w)^2).

LaTeX

$$$$\\operatorname{dist}(z,w) = \\sqrt{ (\\Re z - \\Re w)^{2} + (\\Im z - \\Im w)^{2} }$$$$

Lean4

theorem dist_eq_re_im (z w : ℂ) : dist z w = √((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2) :=
  by
  rw [sq, sq]
  rfl

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