English
Let x and y be elements of WithLp 2 (α × β). Then the distance between x and y is given by the Euclidean combination of the distances of their α- and β-components: edist(x, y) = sqrt(edist(x.fst, y.fst)^2 + edist(x.snd, y.snd)^2).
Русский
Пусть x и y принадлежат WithLp 2(α × β). Тогда расстояние между x и y задано Евклидовым образом через расстояния их компонент: edist(x, y) = sqrt(edist(x.fst, y.fst)^2 + edist(x.snd, y.snd)^2).
LaTeX
$$$\mathrm{edist}\bigl(x,y\bigr) = \bigl( \mathrm{edist}(x_1,y_1)^2 + \mathrm{edist}(x_2,y_2)^2 \bigr)^{1/2}$$$
Lean4
theorem prod_edist_eq_of_L2 (x y : WithLp 2 (α × β)) :
edist x y = (edist x.fst y.fst ^ 2 + edist x.snd y.snd ^ 2) ^ (1 / 2 : ℝ) := by simp [prod_edist_eq_add]
