Commit 2025-09-08 19:22 b81a4772
View on Github →feat: the maximal atlas is closed under restriction (#28701)
If G is a StructureGroupoid that is ClosedUnderRestriction,
if e is a chart in the maximal atlas of G, then so is any restriction e.restr s to an open set s.
In #28793, I will use this to give a more natural constructor for "f is an immersion at x".
From the path towards smooth immersions, embeddings and embedded submanifolds.