nndist_eq_of_L1 — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem nndist_eq_of_L1 (x y : PiLp 1 β) : nndist x y = ∑ i, nndist (x i) (y i) :=
  NNReal.eq <| by push_cast; exact dist_eq_of_L1 _ _

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