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_preimage'View on Github →