Commit 2025-09-09 20:21 d0e35879

View on Github →

feat(Topology): some IsOpenMap lemmas (#27527) Some lemmas for IsOpenMap that I needed. I've also added variants for IsClosedMap to maintain symmetry in the API.

Estimated changes

Modified Mathlib/Topology/Connected/TotallyDisconnected.lean

Modified Mathlib/Topology/Constructions.lean

added theorem Continuous.subtype_coind

added theorem IsClosed.isClosedMap_inclusion

added theorem IsClosedMap.codRestrict

added theorem IsClosedMap.mapsToRestrict

added theorem IsClosedMap.restrict

added theorem IsClosedMap.subtype_coind

added theorem IsClosedMap.subtype_map

added theorem IsClosedMap.subtype_mk

added theorem IsOpen.isOpenMap_inclusion

added theorem IsOpenMap.codRestrict

added theorem IsOpenMap.mapsToRestrict

added theorem IsOpenMap.subtype_coind

added theorem IsOpenMap.subtype_map

added theorem IsOpenMap.subtype_mk

Modified Mathlib/Topology/ContinuousOn.lean

added theorem ContinuousOn.mapsToRestrict

deleted theorem ContinuousOn.restrict_mapsTo

Modified Mathlib/Topology/EMetricSpace/Lipschitz.lean

Modified Mathlib/Topology/Homeomorph/Lemmas.lean

Modified Mathlib/Topology/PartialHomeomorph.lean