Commit 2024-09-03 10:20 fa76f8ba
View on Github →feat: the product of boundaryless manifolds is boundaryless (#14972) To facilitate this change, performs some preliminary clean-up to this file.
- Rename
boundary_eq_complement_interior
tocompl_interior
and flip its direction. (Happy to add a deprecation warning if desired.) - Add the analogous lemma
ModelWithCorners.compl_boundary
- Add
Boundaryless.iff_boundary_eq_empty
:M
is boundaryless iff its boundary is empty - Trivially generalise the lemma about the boundary of product manifolds to
BoundarylessManifold
(not just the model being boundaryless). - Move these lemmas into the
ModelWithCorners
namespace, where they arguably belong. Extracted from my in-progress bordism theory branch.