English
Negation acts coordinatewise: the first coordinate of -(x) is -(x.fst).
Русский
Отрицание действует по координатам: первая координата -x равна -(x.fst).
LaTeX
$$$(-x).\mathrm{fst} = - x.\mathrm{fst}$$$
Lean4
/-- Endowing the space `WithLp p (α × β)` with the `L^p` edistance. We register this instance
separate from `WithLp.instProdPseudoEMetric` since the latter requires the type class hypothesis
`[Fact (1 ≤ p)]` in order to prove the triangle inequality.
Registering this separately allows for a future emetric-like structure on `WithLp p (α × β)` for
`p < 1` satisfying a relaxed triangle inequality. The terminology for this varies throughout the
literature, but it is sometimes called a *quasi-metric* or *semi-metric*. -/
instance instProdEDist : EDist (WithLp p (α × β)) where
edist f
g :=
if _hp : p = 0 then (if edist f.fst g.fst = 0 then 0 else 1) + (if edist f.snd g.snd = 0 then 0 else 1)
else
if p = ∞ then edist f.fst g.fst ⊔ edist f.snd g.snd
else (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal)
