Theorem PartialHomeomorph.extend_preimage_mem_nhds_of_mem_nhdsWithin

Modification history

2025-07-04 16:21
Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
feat: more API on manifolds (#26501)
Added PartialHomeomorph.extend_preimage_mem_nhds_of_mem_nhdsWithinView on Github →