Commit 2025-02-20 10:22 c97217ff

feat: add Is{Open,Closed}Embedding.sum_elim (#22070) The necessary pieces are all in mathlib (for the open and/or the closed case), this is just a matter of putting them together. This comes up when constructing the smooth boundary of a disjoint union. Extracted from #22059; from my bordism theory project.