edist_eq — Mathlib

English

The edist (Euclidean distance in the E-metric) in a finite product is the square root of the sum of coordinate edists squared: edist(x,y) = sqrt( ∑_i edist(x_i,y_i)^2 ).

Русский

Edist в конечном произведении равно корню из суммы квадратов по координатам: edist(x,y) = sqrt( ∑_i edist(x_i,y_i)^2 ).

LaTeX

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

Lean4

theorem edist_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n] (x y : EuclideanSpace 𝕜 n) :
    edist x y = (∑ i, edist (x i) (y i) ^ 2) ^ (1 / 2 : ℝ) :=
  PiLp.edist_eq_of_L2 x y

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