isometry_ofLp_infty — Mathlib

English

The map from the ∞-case of the Lp product to the product space is an isometry.

Русский

Отображение для случая ∞ является изометрией.

LaTeX

$$Isometry (@ofLp ∞ (∀ i, β i))$$

Lean4

theorem isometry_ofLp_infty [∀ i, PseudoEMetricSpace (β i)] : Isometry (@ofLp ∞ (∀ i, β i)) := fun x y =>
  le_antisymm (by simpa only [ENNReal.coe_one, one_mul] using lipschitzWith_ofLp ∞ β x y)
    (by
      simpa only [ENNReal.div_top, ENNReal.toReal_zero, NNReal.rpow_zero, ENNReal.coe_one, one_mul] using
        antilipschitzWith_ofLp ∞ β x y)

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