nndist_eq_of_L2 — Mathlib

English

For x,y ∈ PiLp 2 β, the squared NNReal distance equals the sum of coordinatewise squared NNReal distances: nndist(x,y)^2 = ∑_i nndist(x_i,y_i)^2.

Русский

Для x,y ∈ PiLp 2 β квадрат расстояния NNReal равен сумме координатных квадратов: nndist(x,y)^2 = ∑_i nndist(x_i,y_i)^2.

LaTeX

$$$\operatorname{nndist}(x,y)^{2} = \sum_{i\in ι} \operatorname{nndist}(x_i,y_i)^{2},\quad x,y\in PiLp\;2\;β$$$

Lean4

theorem nndist_eq_of_L2 (x y : PiLp 2 β) : nndist x y = NNReal.sqrt (∑ i, nndist (x i) (y i) ^ 2) :=
  NNReal.eq <| by
    push_cast
    exact dist_eq_of_L2 _ _

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