Commit 2025-07-03 22:17 53ab92ac

View on Github →

feat: MDifferentiableOn.iUnion (#26687) Analogue of #26673 for MDifferentiableOn. Transitive mathlib clean-up from the path towards geodesics and the Levi-Civita connection.

Estimated changes

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

added theorem MDifferentiableOn.iUnion_of_isOpen

added theorem MDifferentiableOn.union_of_isOpen

added theorem mdifferentiableOn_iUnion_iff_of_isOpen

added theorem mdifferentiableOn_union_iff_of_isOpen

added theorem mdifferentiable_of_mdifferentiableOn_iUnion_of_isOpen

added theorem mdifferentiable_of_mdifferentiableOn_union_of_isOpen