uniformEquivProd — Mathlib

English

There is a uniform isomorphism between WithLp p (α × β) and α × β, given by uniformEquivProd p α β.

Русский

Существует равномерный изоморфизм между WithLp p (α × β) и α × β, задаваемый uniformEquivProd p α β.

LaTeX

$$$ \\mathrm{WithLp}_{p}(\\alpha \\times \\beta) \\cong_{u} (\\alpha \\times \\beta). $$$

Lean4

/-- `WithLp.equiv` as a uniform isomorphism. -/
def uniformEquivProd : WithLp p (α × β) ≃ᵤ α × β
    where
  toEquiv := WithLp.equiv p (α × β)
  uniformContinuous_toFun := prod_uniformContinuous_ofLp p α β
  uniformContinuous_invFun := prod_uniformContinuous_toLp p α β

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