English
Let M and M' be manifolds with their tangent bundles TM and TM'. The canonical identification between the tangent bundle of the product M × M' and the product of tangent bundles TM × TM' is a smooth map of class C^n. In particular, there is a smooth equivalence (and its inverse) between T(M × M') and TM × TM'.
Русский
Пусть M и M' — многообразия; касательныеBundle TM и TM'. Каноническое тождество между касательными к произведению T(M × M') и произведением касательных TM × TM' является гладким отображением класса C^n. В частности, существует гладкое биективное соответствие между T(M × M') и TM × TM', и у него есть гладкая обратная карта.
LaTeX
$$$\operatorname{ContMDiff}_n\left((I.\mathrm{prod} I').\mathrm{tangent},\; I.\mathrm{tangent}.\mathrm{prod} I'.\mathrm{tangent},\; n,\; \operatorname{equivTangentBundleProd}(I,M,I',M')\right)$$$
Lean4
/-- The canonical equivalence between the tangent bundle of a product and the product of
tangent bundles is smooth. -/
theorem contMDiff_equivTangentBundleProd :
ContMDiff (I.prod I').tangent (I.tangent.prod I'.tangent) n (equivTangentBundleProd I M I' M') :=
by
rw [equivTangentBundleProd_eq_tangentMap_prod_tangentMap]
exact (contMDiff_fst.contMDiff_tangentMap le_rfl).prodMk (contMDiff_snd.contMDiff_tangentMap le_rfl)
