Theorem OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin'

Modification history

2026-02-27 22:05

Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

feat(Geometry/Manifold): API for extended coordinate changes (#35391) …

Deleted OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin'View on Github →

2025-10-02 09:10

Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

chore: rename PartialHomeomorph to OpenPartialHomeomorph (#29113) …

Added OpenPartialHomeomorph.extend_coord_change_source_mem_nhdsWithin'View on Github →