Commit 2026-02-23 10:04 1d554415
View on Github →feat: support products and disjoint unions in the differential geometry elaborators (#30463) Add support for inferring a model with corners on
- products of manifolds
- disjoint unions of manifolds
- an open subset of a manifold Note that these can be nested (e.g., a product with multiple factors, a disjoint union of four manifolds or combinations of these). For binary products of normed spaces, we intentionally refuse to infer a model with corners, as there are two different possible options which are propositionally, but not definitionally equal. For now, we emit a warning to this effect instead. A future PR may remove it (and infer one of these variants): see zulip discussion. This PR completes an important milestone: models with corners are now inferred for all instances mathlib knows about! Update the module doc-string accordingly. A future PR will golf mathlib using these elaborators.