English
The tangent bundle core is ContMDiff along I, given manifold structure conditions, ensuring a smooth structure on coordinate changes.
Русский
Ядро касательного расслоения сплошной (ContMDiff) по отношению к I при заданной структуре многообразия обеспечивает гладкую структуру координатных изменений.
LaTeX
$$ContMDiff tangentBundleCore I M$$
Lean4
/-- The canonical identification between the tangent bundle to the model space and the product,
as a homeomorphism. For the diffeomorphism version, see `tangentBundleModelSpaceDiffeomorph`. -/
def tangentBundleModelSpaceHomeomorph : TangentBundle I H ≃ₜ ModelProd H E :=
{
TotalSpace.toProd H
E with
continuous_toFun := by
let p : TangentBundle I H := ⟨I.symm (0 : E), (0 : E)⟩
have : Continuous (chartAt (ModelProd H E) p) :=
by
rw [← continuousOn_univ]
convert (chartAt (ModelProd H E) p).continuousOn
simp only [TangentSpace.fiberBundle, mfld_simps]
simpa only [mfld_simps] using this
continuous_invFun := by
let p : TangentBundle I H := ⟨I.symm (0 : E), (0 : E)⟩
have : Continuous (chartAt (ModelProd H E) p).symm :=
by
rw [← continuousOn_univ]
convert (chartAt (ModelProd H E) p).symm.continuousOn
simp only [mfld_simps]
simpa only [mfld_simps] using this }
