English
The composition of two ContinuousMulEquiv is a ContinuousMulEquiv; i.e., given e1: M ≃ₜ* N and e2: N ≃ₜ* L, their trans is a ContinuousMulEquiv M ≃ₜ* L.
Русский
Объединение двух непрерывных мультиэквивалентов даёт ещё один непрерывный мультиэквивалент: e1.trans e2: M ≃ₜ* L.
LaTeX
$$The composition of two ContinuousMulEquiv is a ContinuousMulEquiv.$$
Lean4
/-- The composition of two ContinuousMulEquiv. -/
@[to_additive /-- The composition of two ContinuousAddEquiv. -/
]
def trans (cme1 : M ≃ₜ* N) (cme2 : N ≃ₜ* L) : M ≃ₜ* L
where
__ := cme1.toMulEquiv.trans cme2.toMulEquiv
continuous_toFun := by convert Continuous.comp cme2.continuous_toFun cme1.continuous_toFun
continuous_invFun := by convert Continuous.comp cme1.continuous_invFun cme2.continuous_invFun
