Commit 2026-06-19 13:16 01469fac

View on Github →

feat(Geometry/Manifold/Notation): add (d)elaborators for UniqueMDiffOn and UniqueMDiffWithinAt (#40748) This PR adds elaborators and delaborators for UniqueMDiffOn and UniqueMDiffWithinAt. The elaborators currently don't work for finding a model with corners on TotalSpaces since they don't provide baseInfo. This should hopefully be fixed by #40047.

Estimated changes

modified theorem IsOpen.uniqueMDiffOn
modified theorem IsOpen.uniqueMDiffWithinAt
modified theorem UniqueMDiffOn.inter
modified theorem UniqueMDiffOn.prod
modified theorem UniqueMDiffWithinAt.inter'
modified theorem UniqueMDiffWithinAt.inter
modified theorem UniqueMDiffWithinAt.mono
modified theorem mfderivWithin_eq_mfderiv
modified theorem mfderivWithin_subset
modified theorem uniqueMDiffOn_univ
modified theorem uniqueMDiffWithinAt_univ
modified theorem mvfderivWithin_neg
modified theorem mvfderivWithin_zero
modified theorem mfderivWithin_id
modified theorem mfderivWithin_neg
modified theorem mfderivWithin_sumInl
modified theorem mfderivWithin_sumInr
modified theorem mfderivWithin_sumSwap
modified theorem tangentMapWithin_id