English
There exists a canonical diffeomorphism between the tangent bundle of the model space and the ModelProd, given by the total space to product map.
Русский
Существует канонический диффеоморфизм между касательным расхождением модельного пространства и ModelProd, задаваемый отображением TotalSpace.toProd.
LaTeX
$$$tangentBundleModelSpaceDiffeomorph\\ I\\ H\\ (n) : TangentBundle\\ I\\ H \\simeq^n ModelProd H E$$$
Lean4
/-- The canonical identification between the tangent bundle to the model space and the product,
as a diffeomorphism -/
def tangentBundleModelSpaceDiffeomorph (n : ℕ∞) : TangentBundle I H ≃ₘ^n⟮I.tangent, I.prod 𝓘(𝕜, E)⟯ ModelProd H E
where
__ := TotalSpace.toProd H E
contMDiff_toFun := contMDiff_tangentBundleModelSpaceHomeomorph
contMDiff_invFun := contMDiff_tangentBundleModelSpaceHomeomorph_symm
