Commit 2025-11-06 16:54 574e293e

View on Github →

feat: mfderiv of Sum.swap (#31276) To be used to simplify the proof of #31200, thus transitively part of my bordism theory project.

Estimated changes

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

added theorem hasMFDerivAt_sumSwap

added theorem mfderivWithin_sumSwap

added theorem mfderiv_sumSwap

added theorem writtenInExtChartAt_sumSwap_eventuallyEq_id

Modified Mathlib/Topology/NhdsWithin.lean

added theorem mem_nhdsWithin_inter_self

added theorem mem_nhdsWithin_self_inter