prod_nndist_eq_of_L1 — Mathlib

English

For x,y ∈ WithLp 1 (α × β), the NN-distance equality holds (same as previous): nndist(x,y) = nndist(x.fst,y.fst) + nndist(x.snd,y.snd).

Русский

Для x,y ∈ WithLp 1 (α × β) выполняется равенство NN-расстояний (то же): nndist(x,y) = nndist(x.fst,y.fst) + nndist(x.snd,y.snd).

LaTeX

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

Lean4

theorem prod_nndist_eq_of_L1 (x y : WithLp 1 (α × β)) : nndist x y = nndist x.fst y.fst + nndist x.snd y.snd :=
  NNReal.eq <| by
    push_cast
    exact prod_dist_eq_of_L1 _ _

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