English
Product of two transported diffeomorphisms yields a transported diffeomorphism on the product spaces with the expected projection maps.
Русский
Произведение двух перенесённых диффеоморфизмов даёт перенесённый диффеоморфизм на произведениях пространств.
LaTeX
$$$h_1 : M \to M',\; h_2 : N \to N'\quad\Rightarrow\quad (h_1 \prod h_2) : (M\times N) \to (M'\times N')$ is a transported diffeomorphism$$
Lean4
/-- Product of two diffeomorphisms. -/
def prodCongr (h₁ : M ≃ₘ^n⟮I, I'⟯ M') (h₂ : N ≃ₘ^n⟮J, J'⟯ N') : (M × N) ≃ₘ^n⟮I.prod J, I'.prod J'⟯ M' × N'
where
contMDiff_toFun := (h₁.contMDiff.comp contMDiff_fst).prodMk (h₂.contMDiff.comp contMDiff_snd)
contMDiff_invFun := (h₁.symm.contMDiff.comp contMDiff_fst).prodMk (h₂.symm.contMDiff.comp contMDiff_snd)
toEquiv := h₁.toEquiv.prodCongr h₂.toEquiv
