Commit 2025-01-11 05:59 c0cb03aa

feat: disjoint union of charted spaces (#20619) As the main technical tool to do so, we introduce a new definition PartialHomeomorph.lift_openEmbedding, lifting a PartialHomeomorph under an OpenEmbedding. (The left or right inclusion into a disjoint union are open embeddings; this abstract allows proving lemmas only once, and avoids having to deal with subtypes.) From the bordism theory project branch: future steps include proving that the disjoint union of C^n manifolds is a C^n manifold.