homeomorphProd — Mathlib

English

There is a natural homeomorphism between WithLp p (α × β) and α × β, given by the product of the coordinate projections.

Русский

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

LaTeX

$$$$\text{homeomorphProd} : WithLp p (α × β) \simeq_t α × β.$$$$

Lean4

/-- `WithLp.equiv` as a homeomorphism. -/
def homeomorphProd : WithLp p (α × β) ≃ₜ α × β
    where
  toEquiv := WithLp.equiv p (α × β)
  continuous_toFun := prod_continuous_ofLp p α β
  continuous_invFun := prod_continuous_toLp p α β

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