Commit 2024-12-04 17:24 41cbc10a

View on Github →

feat: unique differentiability of preimages under projection doesn't need the bundle to be smooth (#19682)

Estimated changes

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

Modified Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean

modified theorem Trivialization.mdifferentiable

added theorem UniqueMDiffOn.bundle_preimage

deleted theorem UniqueMDiffOn.smooth_bundle_preimage

added theorem UniqueMDiffWithinAt.bundle_preimage'

added theorem UniqueMDiffWithinAt.bundle_preimage

deleted theorem UniqueMDiffWithinAt.smooth_bundle_preimage'

deleted theorem UniqueMDiffWithinAt.smooth_bundle_preimage