Commit 2026-06-19 13:51 0c7d9c10

View on Github →

chore(Geometry/Manifold/ContMDiff/Defs): use variable more (#40798) The file uses x' : M and y : M' throughout: extract this into a variable to declutter statements.

Estimated changes

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

modified theorem contMDiffAt_iff_target_of_mem_source

modified theorem contMDiffWithinAt_iff_image

modified theorem contMDiffWithinAt_iff_of_mem_maximalAtlas

modified theorem contMDiffWithinAt_iff_target_of_mem_source