English
There is an isometry for p = ∞: prod_isometry_ofLp_infty asserts that OfLp ∞ on the product is an isometry.
Русский
Для p = ∞ отображение OfLp на произведении является изометрией.
LaTeX
$$$ \\text{Isometry}(\\operatorname{ofLp}_{\\infty} (\\alpha \\times \\beta)) $$$
Lean4
theorem prod_isometry_ofLp_infty [PseudoEMetricSpace α] [PseudoEMetricSpace β] : Isometry (@ofLp ∞ (α × β)) :=
fun x y =>
le_antisymm (by simpa only [ENNReal.coe_one, one_mul] using prod_lipschitzWith_ofLp ∞ α β x y)
(by
simpa only [ENNReal.div_top, ENNReal.toReal_zero, NNReal.rpow_zero, ENNReal.coe_one, one_mul] using
prod_antilipschitzWith_ofLp ∞ α β x y)