English
The collection of all M ≃ₘ^n⟮I,J⟯ N diffeomorphisms carries a natural continuous map structure; i.e., every such morphism is a continuous map.
Русский
Собрание всех диффеоморфизмов M ≃ₘ^n⟮I,J⟯ N естественно несет структуру непрерывного отображения; то есть каждый такой морфизм является непрерывной картой.
LaTeX
$$$\text{ContinuousMapClass}(Diffeomorph I J M N)\, M\, N$$$
Lean4
/-- Composition of two diffeomorphisms. -/
@[trans]
protected def trans (h₁ : M ≃ₘ^n⟮I, I'⟯ M') (h₂ : M' ≃ₘ^n⟮I', J⟯ N) : M ≃ₘ^n⟮I, J⟯ N
where
contMDiff_toFun := h₂.contMDiff.comp h₁.contMDiff
contMDiff_invFun := h₁.contMDiff_invFun.comp h₂.contMDiff_invFun
toEquiv := h₁.toEquiv.trans h₂.toEquiv
