prod_nndist_eq_of_L2 — Mathlib

English

For x,y ∈ WithLp 2 (α × β), the NN-distance satisfies nndist(x,y) = sqrt(nndist(x.fst,y.fst)^2 + nndist(x.snd,y.snd)^2).

Русский

Для x,y ∈ WithLp 2 (α × β) NN-расстояние удовлетворяет nndist(x,y) = sqrt(nndist(x1,y1)^2 + nndist(x2,y2)^2).

LaTeX

$$$\mathrm{nndist}(x,y) = \sqrt{\mathrm{nndist}(x_{\mathrm{fst}},y_{\mathrm{fst}})^2 + \mathrm{nndist}(x_{\mathrm{snd}},y_{\mathrm{snd}})^2}$$$

Lean4

theorem prod_nndist_eq_of_L2 (x y : WithLp 2 (α × β)) :
    nndist x y = NNReal.sqrt (nndist x.fst y.fst ^ 2 + nndist x.snd y.snd ^ 2) :=
  NNReal.eq <| by
    push_cast
    exact prod_dist_eq_of_L2 _ _

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