prod_dist_eq_of_L1 — Mathlib

English

For x,y ∈ WithLp 1 (α × β), the NN-distance equals the sum of the componentwise NN-distances: nndist(x,y) = nndist(x.fst,y.fst) + nndist(x.snd,y.snd).

Русский

Для x,y ∈ WithLp 1 (α × β) расстояние по NN-метрике равно сумме 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_dist_eq_of_L1 (x y : WithLp 1 (α × β)) : dist x y = dist x.fst y.fst + dist x.snd y.snd := by
  simp_rw [dist_eq_norm, prod_norm_eq_of_L1, sub_fst, sub_snd]

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