Commit 2026-06-16 13:03 bf81df9a

feat: an explicit criterion for membership in the maximal atlas of a C^n manifold (#40632) Add an explicit characterisation, that an OpenPartialHomeomorph phi lies in the maximal atlas of a C^n manifold if both phi and phi.symm are C^n on their source. This can be useful to prove that certain explicit maps are in the maximal atlas, so prove some maps are immersions. Motivating examples are #29077 (for the inclusion of a closed interval [a, b] into the real numbers) and for a manual proof that diffeomorphisms are immersions. Along the way, rename contMDiff_model and its inverse cousin contMDiffOn_model_symm to match the naming convention, and golf their proofs.