Commit 2023-07-13 04:03 625a3a62

View on Github →

feat: port Geometry.Manifold.ContMdiffMfderiv (#5496)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

added theorem ContMDiff.contMDiff_tangentMap

added theorem ContMDiff.continuous_tangentMap

added theorem ContMDiffAt.mfderiv_apply

added theorem ContMDiffAt.mfderiv_const

added theorem ContMDiffOn.contMDiffOn_tangentMapWithin

added theorem ContMDiffOn.contMDiffOn_tangentMapWithin_aux

added theorem ContMDiffOn.continuousOn_tangentMapWithin

added theorem ContMDiffOn.continuousOn_tangentMapWithin_aux

added theorem TangentBundle.tangentMap_tangentBundle_pure

Modified Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean