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

  1. isOpen_extChartAt_source
  2. extChartAt_source_mem_nhds
  3. extChartAt_source_mem_nhds' (extChartAt I x).target fails to be open near manifold boundary points, but we recover the nice lemmas when I.Boundaryless.

Estimated changes