Commit 2023-12-19 12:55 1150c07e

feat: interior and boundary of a manifold (#8624) We use the standard definition, with respect to the preferred charts at each point. Open-ness of the interior is non-trivial, hence left to a future PR:

• for instance, in finite dimensions this requires e.g. knowing the homology of spheres, which mathlib doesn't yet have.