dist_mk — Mathlib

English

The distance between two points in the complex plane, given by (x1,y1) and (x2,y2), equals the Euclidean distance: sqrt((x1 - x2)^2 + (y1 - y2)^2).

Русский

Расстояние между точками (x1,y1) и (x2,y2) на комплексной плоскости равно евклидову расстоянию: sqrt((x1 - x2)^2 + (y1 - y2)^2).

LaTeX

$$$\\forall x_{1}, y_{1}, x_{2}, y_{2} \\in \\mathbb{R}, \\operatorname{dist}(\\operatorname{mk}(x_{1},y_{1}), \\operatorname{mk}(x_{2},y_{2})) = \\sqrt{(x_{1}-x_{2})^{2} + (y_{1}-y_{2})^{2}}$$$

Lean4

@[simp]
theorem dist_mk (x₁ y₁ x₂ y₂ : ℝ) : dist (mk x₁ y₁) (mk x₂ y₂) = √((x₁ - x₂) ^ 2 + (y₁ - y₂) ^ 2) :=
  dist_eq_re_im _ _

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