dist_sq_eq — Mathlib

English

In a finite product, the square of the distance equals the sum of the squares of coordinate distances: dist(x,y)^2 = ∑_i dist(x_i,y_i)^2.

Русский

Квадрат расстояния равен сумме квадратов координатных расстояний: dist(x,y)^2 = ∑_i dist(x_i,y_i)^2.

LaTeX

$$$\operatorname{dist}(x,y)^2 = \sum_i \operatorname{dist}(x_i,y_i)^2$$$

Lean4

theorem dist_sq_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n] (x y : EuclideanSpace 𝕜 n) :
    dist x y ^ 2 = ∑ i, dist (x i) (y i) ^ 2 :=
  PiLp.dist_sq_eq_of_L2 x y

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