Commit 2024-01-27 11:43 ae8f621c

View on Github →

feat: four small lemmas about extended charts (#10001) From sphere-eversion; I'm just submitting them.

Estimated changes

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

added theorem PartialHomeomorph.extend_image_nhd_mem_nhds_of_boundaryless

added theorem PartialHomeomorph.map_extend_nhds_of_boundaryless

added theorem extChartAt_image_nhd_mem_nhds_of_boundaryless

added theorem map_extChartAt_nhds_of_boundaryless