Commit 2026-06-17 14:21 7d46b4c5

View on Github →

chore: rename {OpenPartialHomeomorph,PartialEquiv}.map_source'' (#40717) The new name avoids a double prime and also matches the naming convention. As suggested here.

Estimated changes

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/Logic/Equiv/PartialEquiv.lean

added theorem PartialEquiv.image_source_subset

deleted theorem PartialEquiv.map_source''

Modified Mathlib/Topology/OpenPartialHomeomorph/Defs.lean

added theorem OpenPartialHomeomorph.image_source_subset

deleted theorem OpenPartialHomeomorph.map_source''