Commit 2025-09-02 08:17 bd5c1e57

View on Github →

feat(Geometry/Manifold/ContMDiff): add product lemmas for ContMDiff (#28292) Add product lemmas for ContMDiff. These are analogous to the corresponding lemmas for Continuous in Mathlib.Topology.Constructions.SumProd. This is upstreamed from https://github.com/girving/ray.

Estimated changes

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

added theorem ContMDiff.curry_left

added theorem ContMDiff.curry_right

added theorem ContMDiffAt.comp₂

added theorem ContMDiffAt.comp₂_of_eq

added theorem ContMDiffAt.curry_left

added theorem ContMDiffAt.curry_right

added theorem ContMDiffOn.curry_left

added theorem ContMDiffOn.curry_right

added theorem ContMDiffWithinAt.comp₂

added theorem ContMDiffWithinAt.comp₂_of_eq

added theorem ContMDiffWithinAt.curry_left

added theorem ContMDiffWithinAt.curry_right