English
The distance from a point to itself is zero: edist f f = 0 for any f ∈ WithLp p (α × β).
Русский
Расстояние от точки к самой себе равно нулю: edist f f = 0 для любого f ∈ WithLp p (α × β).
LaTeX
$$$$\operatorname{edist} f f = 0.$$$$
Lean4
/-- The distance from one point to itself is always zero.
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_self (f : WithLp p (α × β)) : edist f f = 0 :=
by
rcases p.trichotomy with (rfl | rfl | h)
· classical simp
· simp [prod_edist_eq_sup]
· simp [prod_edist_eq_add h, ENNReal.zero_rpow_of_pos h, ENNReal.zero_rpow_of_pos (inv_pos.2 <| h)]
