English
There is a natural continuous linear isomorphism between the Lp-sum space PiLp p β and the product space ∀ i, β_i, provided by the canonical linear equivalence induced by WithLp.
Русский
Существует естественное непрерывно-линейное изоморфизм между пространством PiLp p β и произведением по i β_i, реализованный каноническим линейным эквивалентом, порождённым WithLp.
LaTeX
$$$\mathrm{PiLp}(p, \beta) \cong_L^{(\mathbb{𝕜})} \prod_{i} \beta_i$$$
Lean4
/-- `WithLp.linearEquiv` as a continuous linear equivalence. -/
@[simps! -fullyApplied apply symm_apply]
def continuousLinearEquiv : PiLp p β ≃L[𝕜] ∀ i, β i
where
toLinearEquiv := WithLp.linearEquiv _ _ _
continuous_toFun := continuous_ofLp _ _
continuous_invFun := continuous_toLp p _
