English
There exists a continuous linear equivalence between WithLp p (α × β) and α × β, with the forward map given by WithLp.linearEquiv and both directions continuous id.
Русский
Существует непрерывное линейное эквивалентное отображение между WithLp p (α × β) и α × β, задаваемое WithLp.linearEquiv и единичными отображениями в обе стороны.
LaTeX
$$$ \\mathrm{WithLp}_{p}(\\alpha \\times \\beta) \\simeq_{L[\\mathfrak{K}]} \\alpha \\times \\beta. $$$
Lean4
/-- `WithLp.equiv` as a continuous linear equivalence. -/
-- This is not specific to products and should be generalised!
@[simps!]
def prodContinuousLinearEquiv : WithLp p (α × β) ≃L[𝕜] α × β
where
toLinearEquiv := WithLp.linearEquiv _ _ _
continuous_toFun := continuous_id
continuous_invFun := continuous_id
