prod_isometry_ofLp_infty — Mathlib

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)

Похожие утверждения