Commit 2024-02-22 00:33 911c1691
View on Github →feat: Lemmas about (extChartAt I x).target
being open if we're boundaryless (#10840)
(extChartAt I x).source
is always open, so there are nice lemmas like
isOpen_extChartAt_source
extChartAt_source_mem_nhds
extChartAt_source_mem_nhds'
(extChartAt I x).target
fails to be open near manifold boundary points, but we recover the nice lemmas whenI.Boundaryless
.