prod_edist_eq_of_L1 — Mathlib

English

For x,y ∈ WithLp 1 (α × β), the EN-distances add: edist(x,y) = edist(x.fst,y.fst) + edist(x.snd,y.snd).

Русский

Для x,y ∈ WithLp 1 (α × β) расстояние edist складывается: edist(x,y) = edist(x.fst,y.fst) + edist(x.snd,y.snd).

LaTeX

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

Lean4

theorem prod_edist_eq_of_L1 (x y : WithLp 1 (α × β)) : edist x y = edist x.fst y.fst + edist x.snd y.snd := by
  simp [prod_edist_eq_add]

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