Commit 2026-07-12 10:17 b95982f4

chore(Geometry/Manifold/ContMDiff/Atlas): generalise mem_maximalAtlas_of_contMDiffOn and friends (#40720) These lemmas were only stated about maps on the underlying topological space H. They should be generalised to include charts of the manifold M. This comes up when proving that diffeomorphisms are immersions (by hand) and also when defining quotient manifolds. Follow-up to #40632.