English
Let E1: M1 ≃SL[σ12] M2 and E2: M2 ≃SL[σ23] M3 be continuous linear equivalences; then their composite E1.trans E2 is a continuous linear equivalence M1 ≃SL[σ13] M3, i.e. the composition of two continuous linear equivalences is again a continuous linear equivalence.
Русский
Пусть E1: M1 ≃SL[σ12] M2 и E2: M2 ≃SL[σ23] M3 — непрерывные линейные эквиваленты; тогда их композиция E1.trans E2 является непрерывным линейным эквивалентом M1 ≃SL[σ13] M3, то есть композиция двух непрерывных линейных эквивалентов снова непрерывный линейный эквивалент.
LaTeX
$$$$\text{If } E_1: M_1 \simeq_{\sigma_{12}} M_2 \text{ and } E_2: M_2 \simeq_{\sigma_{23}} M_3, \text{ then } E_1 \circ E_2: M_1 \simeq_{\sigma_{13}} M_3 \text{ is a continuous linear equivalence},$$ where $\sigma_{13}$ is the appropriate composed ring homomorphism. $$$$
Lean4
/-- The composition of two continuous linear equivalences as a continuous linear equivalence. -/
@[trans]
protected def trans (e₁ : M₁ ≃SL[σ₁₂] M₂) (e₂ : M₂ ≃SL[σ₂₃] M₃) : M₁ ≃SL[σ₁₃] M₃ :=
{
e₁.toLinearEquiv.trans
e₂.toLinearEquiv with
continuous_toFun := e₂.continuous_toFun.comp e₁.continuous_toFun
continuous_invFun := e₁.continuous_invFun.comp e₂.continuous_invFun }
