English
The product of two continuous linear equivalences is a continuous linear equivalence between product spaces.
Русский
Произведение двух непрерывных линейных эквивалентов образует непрерывный линейный эквивалент между произведениями пространств.
LaTeX
$$$$e: M_1 \simeq_{\sigma_{12}} M_2, \quad e': M_3 \simeq_{\sigma_{34}} M_4 \quad\Rightarrow\quad e.prodCongr e': M_1 \times M_3 \simeq_{\sigma} M_2 \times M_4,$$ где правая часть задаётся компонентно.$$
Lean4
/-- Product of two continuous linear equivalences. The map comes from `Equiv.prodCongr`. -/
def prodCongr [Module R₁ M₂] [Module R₁ M₃] [Module R₁ M₄] (e : M₁ ≃L[R₁] M₂) (e' : M₃ ≃L[R₁] M₄) :
(M₁ × M₃) ≃L[R₁] M₂ × M₄ :=
{
e.toLinearEquiv.prodCongr
e'.toLinearEquiv with
continuous_toFun := e.continuous_toFun.prodMap e'.continuous_toFun
continuous_invFun := e.continuous_invFun.prodMap e'.continuous_invFun }
