Mathlib Changelog
v4
Changelog
About
Github
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