Theorem UniqueMDiffWithinAt.bundle_preimage'

Modification history

2026-06-23 08:28

Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean

feat: properly support inferring a model with corners on a `Bundle.TotalSpace` (#40047) …

Modified UniqueMDiffWithinAt.bundle_preimage'View on Github →

2026-06-19 13:16

Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean

feat(Geometry/Manifold/Notation): add (d)elaborators for `UniqueMDiffOn` and `UniqueMDiffWithinAt` (#40748) …

Modified UniqueMDiffWithinAt.bundle_preimage'View on Github →

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 →