prod_dist_eq_of_L2 — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem prod_dist_eq_of_L2 (x y : WithLp 2 (α × β)) : dist x y = √(dist x.fst y.fst ^ 2 + dist x.snd y.snd ^ 2) := by
  simp_rw [dist_eq_norm, prod_norm_eq_of_L2, sub_fst, sub_snd]

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