# 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`

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.