Commit 2024-04-01 15:04 8667e5da

View on Github →

feat(Topology/Maps): add *.of_subsingleton and *.of_isEmpty (#11818) Also use OpenEmbedding.of_subsingleton to golf AlgebraicGeometry.isOpenImmersion_of_isEmpty.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/Topology/Maps.lean

added theorem Embedding.of_subsingleton

added theorem Inducing.of_subsingleton

added theorem IsOpenMap.of_isEmpty

added theorem OpenEmbedding.of_isEmpty