English
There is a canonical linear homeomorphism between EuclideanSpace 𝕜 (Fin (n + m)) and EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m), i.e., a finite-dimensional splitting into two blocks.
Русский
Существует канонический линейный гомеоморфизм между EuclideanSpace 𝕜 (Fin (n + m)) и EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m).
LaTeX
$$$\mathrm{finAddEquivProd} : EuclideanSpace 𝕜 (Fin (n+m)) \simeq_L[𝕜] EuclideanSpace 𝕜 (Fin n) \times EuclideanSpace 𝕜 (Fin m)$$$
Lean4
/-- The canonical linear homeomorphism between `EuclideanSpace 𝕜 (Fin (n + m))` and
`EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m)`. -/
abbrev finAddEquivProd {𝕜 : Type*} [RCLike 𝕜] {n m : ℕ} :
EuclideanSpace 𝕜 (Fin (n + m)) ≃L[𝕜] EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m) :=
(LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 finSumFinEquiv.symm).toContinuousLinearEquiv.trans sumEquivProd
