English
Associativity of products up to continuous linear isomorphism: ((M1×M2)×M3) ≃L[R] M1×M2×M3.
Русский
Ассоциативность произведений до непрерывного линейного эквиваленса: ((M1×M2)×M3) ≃L[R] M1×M2×M3.
LaTeX
$$$$ ((M_1 \times M_2) \times M_3) \simeq_L[R] M_1 \times M_2 \times M_3. $$$$
Lean4
/-- The product of topological modules is associative up to continuous linear isomorphism.
This is `LinearEquiv.prodAssoc` prodAssoc as a continuous linear equivalence. -/
def prodAssoc : ((M₁ × M₂) × M₃) ≃L[R] M₁ × M₂ × M₃
where
toLinearEquiv := LinearEquiv.prodAssoc R M₁ M₂ M₃
continuous_toFun :=
(continuous_fst.comp continuous_fst).prodMk ((continuous_snd.comp continuous_fst).prodMk continuous_snd)
continuous_invFun :=
(continuous_fst.prodMk (continuous_fst.comp continuous_snd)).prodMk (continuous_snd.comp continuous_snd)
