English
Distance is symmetric: edist(f, g) = edist(g, f) for all f, g ∈ WithLp p (α × β).
Русский
Расстояние симметрично: edist(f, g) = edist(g, f) для всех f, g ∈ WithLp p (α × β).
LaTeX
$$$$\operatorname{edist} f g = \operatorname{edist} g f.$$$$
Lean4
/-- The distance is symmetric.
This holds independent of `p` and does not require `[Fact (1 ≤ p)]`. We keep it separate
from `WithLp.instProdPseudoEMetricSpace` so it can be used also for `p < 1`. -/
theorem prod_edist_comm (f g : WithLp p (α × β)) : edist f g = edist g f := by
classical
rcases p.trichotomy with (rfl | rfl | h)
· simp only [prod_edist_eq_card, edist_comm]
· simp only [prod_edist_eq_sup, edist_comm]
· simp only [prod_edist_eq_add h, edist_comm]
