dist_eq — Mathlib

English

The distance between x and y in a finite product of normed spaces is the L2-sum of the coordinate distances: dist(x,y) = sqrt( ∑_i dist(x_i,y_i)^2 ).

Русский

Расстояние между двумя точками в конечном произведении нормированных пространств равно L2-несложению расстояний координат: dist(x,y) = sqrt( ∑_i dist(x_i,y_i)^2 ).

LaTeX

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

Lean4

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

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