English
There exists a natural homeomorphism between the Lp-product of the spaces {β_i} and the Cartesian product ∏_i β_i, given by identifying a function f with its coordinate values (f(i)).
Русский
Существует естественный гомеоморфизм между Lp-образом множества β_i и декартовым произведением ∏_i β_i, задаваемый идентификацией функции f с её координатами (f(i)).
LaTeX
$$$PiLp\ p\, \beta \;\cong_{\mathrm{Top}}\; \prod_{i} \beta_i$$$
Lean4
/-- `WithLp.equiv` as a homeomorphism. -/
def homeomorph [∀ i, TopologicalSpace (β i)] : PiLp p β ≃ₜ (Π i, β i)
where
toEquiv := WithLp.equiv p (Π i, β i)
continuous_toFun := continuous_ofLp p β
continuous_invFun := continuous_toLp p β
