Theorem OpenPartialHomeomorph.contDiffOn_extend_coord_change

Modification history

2026-02-27 22:05
Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
feat(Geometry/Manifold): API for extended coordinate changes (#35391) …
Deleted OpenPartialHomeomorph.contDiffOn_extend_coord_changeView on Github →
2025-10-02 09:10
Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
chore: rename PartialHomeomorph to OpenPartialHomeomorph (#29113) …
Added OpenPartialHomeomorph.contDiffOn_extend_coord_changeView on Github →