Commit 2025-02-20 18:07 b2b26f19

View on Github →

chore: fix naming oversight from #22070 (#22128) Per zulip discussion: these were merged a few hours ago, hence need no deprecations yet.

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean

Modified Mathlib/Topology/Constructions.lean

added theorem Continuous.sumElim

deleted theorem Continuous.sum_elim

added theorem IsClosedEmbedding.sumElim

deleted theorem IsClosedEmbedding.sum_elim

added theorem IsClosedMap.sumElim

deleted theorem IsClosedMap.sum_elim

added theorem IsOpenEmbedding.sumElim

deleted theorem IsOpenEmbedding.sum_elim

added theorem IsOpenMap.sumElim

deleted theorem IsOpenMap.sum_elim

added theorem continuous_sumElim

deleted theorem continuous_sum_elim

added theorem isClosedMap_sumElim

deleted theorem isClosedMap_sum_elim

added theorem isOpenMap_sumElim

deleted theorem isOpenMap_sum_elim

Modified Mathlib/Topology/Homeomorph.lean