English
There exists a canonical linear homeomorphism between EuclideanSpace 𝕜 (ι ⊕ κ) and EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ, identifying the combined index space with the product of the two component spaces.
Русский
Существует каноническое линейное гомеоморфизм между EuclideanSpace 𝕜 (ι ⊕ κ) и EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ, который идентифицирует объединённое множество индексов с произведением двух компонентной пространств.
LaTeX
$$$\mathrm{sumEquivProd} : \EuclideanSpace 𝕜 (ι \oplus κ) \simeq_L[𝕜] \EuclideanSpace 𝕜 ι \times \EuclideanSpace 𝕜 κ$$$
Lean4
/-- The canonical linear homeomorphism between `EuclideanSpace 𝕜 (ι ⊕ κ)` and
`EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ`.
See `PiLp.sumPiLpEquivProdLpPiLp` for the isometry version,
where the RHS is equipped with the Euclidean norm rather than the supremum norm. -/
abbrev sumEquivProd {𝕜 : Type*} [RCLike 𝕜] {ι κ : Type*} [Fintype ι] [Fintype κ] :
EuclideanSpace 𝕜 (ι ⊕ κ) ≃L[𝕜] EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ :=
(PiLp.sumPiLpEquivProdLpPiLp 2 _).toContinuousLinearEquiv.trans <| WithLp.prodContinuousLinearEquiv _ _ _ _
