Commit 2024-09-03 10:20 fa76f8ba

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 to compl_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.