toEquiv_homeomorph — Mathlib

English

The underlying equivalence of the PiLp homeomorphism is exactly the canonical WithLp equivalence between the Lp-product and the product space.

Русский

Граница эквивалентности гомеоморфа PiLp совпадает с каноническим эквивалентом WithLp между Lp-образом и произведением пространств.

LaTeX

$$$(PiLp.homeomorph\ p\ \beta).toEquiv = WithLp.equiv\ p\ (\Pi i,\ beta_i)$$$

Lean4

@[simp]
theorem toEquiv_homeomorph [∀ i, TopologicalSpace (β i)] : (homeomorph p β).toEquiv = WithLp.equiv p (Π i, β i) :=
  rfl

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