Theorem OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn

Modification history

2026-07-12 10:17
Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
chore(Geometry/Manifold/ContMDiff/Atlas): generalise `mem_maximalAtlas_of_contMDiffOn` and friends (#40720) …
Modified OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOnView on Github →
2026-06-16 13:03
Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
feat: an explicit criterion for membership in the maximal atlas of a `C^n` manifold (#40632) …
Added OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOnView on Github →