English
For hp: 0 < p.toReal and f, g ∈ WithLp p (α × β), the distance dist(f, g) equals the p‑norm of the coordinate distances: dist(f, g) = (dist(f.fst, g.fst)^{p.toReal} + dist(f.snd, g.snd)^{p.toReal})^{1/p.toReal}.
Русский
При hp: 0 < p.toReal и f, g ∈ WithLp p (α × β) расстояние dist(f, g) равно p‑норме координатных расстояний: dist(f, g) = (dist(f.fst, g.fst)^{p.toReal} + dist(f.snd, g.snd)^{p.toReal})^{1/p.toReal}.
LaTeX
$$$$\operatorname{dist} f g = \left( \operatorname{dist} f.fst g.fst^{\;p.toReal} + \operatorname{dist} f.snd g.snd^{\;p.toReal} \right)^{1 / p.toReal}$$$$
Lean4
theorem prod_dist_eq_add (hp : 0 < p.toReal) (f g : WithLp p (α × β)) :
dist f g = (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) :=
let hp' := ENNReal.toReal_pos_iff.mp hp
(if_neg hp'.1.ne').trans (if_neg hp'.2.ne)
