Theorem UniqueMDiffWithinAt.bundle_preimage

Modification history

2024-12-04 17:24
Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean
feat: unique differentiability of preimages under projection doesn't need the bundle to be smooth (#19682)
Added UniqueMDiffWithinAt.bundle_preimageView on Github →