nndist_eq — Mathlib

English

The nonnegative distance (nndist) in the L2 direct sum equals the NNReal square root of the sum of the squares of coordinate nonnegative distances: nndist(x,y) = sqrt( ∑_i nndist(x_i,y_i)^2 ).

Русский

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

LaTeX

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

Lean4

theorem nndist_eq {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n] (x y : EuclideanSpace 𝕜 n) :
    nndist x y = NNReal.sqrt (∑ i, nndist (x i) (y i) ^ 2) :=
  PiLp.nndist_eq_of_L2 x y

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