Commit 2025-03-20 10:48 2ad02e6d

View on Github →

feat: weaken differentiability assumptions of manifolds (#22804) Given our definitions, many natural maps between manifolds are C^n even when the manifolds are just C^1, because they are expressed in terms of the canonical charts. This PR takes advantage of this to weaken several assumptions on manifolds from C^n to C^1.

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean

modified theorem contMDiffAt_extChartAt

added theorem contMDiffWithinAt_extChartAt_symm_range_self

added theorem contMDiffWithinAt_extChartAt_symm_target_self

Modified Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

added theorem contMDiffAt_iff_source

added theorem contMDiffWithinAt_iff_source

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

Modified Mathlib/Geometry/Manifold/VectorField/Pullback.lean