English
The composition of two continuous algebra equivalences is a continuous algebra equivalence. If e1: A ≃A[R] B and e2: B ≃A[R] C, then e1 trans e2: A ≃A[R] C is again a continuous algebra equivalence.
Русский
Сложение двух непрерывных алгебраических эквивалентностей приводит к новой непрерывной алгебраической эквивалентности. Пусть e1: A ≃A[R] B и e2: B ≃A[R] C, тогда e1 trans e2: A ≃A[R] C.
LaTeX
$$$(e_1 \mathrm{trans} e_2).toAlgEquiv = e_1.toAlgEquiv.trans e_2.toAlgEquiv$$$
Lean4
/-- The composition of two continuous algebra equivalences. -/
@[trans]
def trans (e₁ : A ≃A[R] B) (e₂ : B ≃A[R] C) : A ≃A[R] C
where
__ := e₁.toAlgEquiv.trans e₂.toAlgEquiv
continuous_toFun := e₂.continuous_toFun.comp e₁.continuous_toFun
continuous_invFun := e₁.continuous_invFun.comp e₂.continuous_invFun
