Commit 2024-08-23 10:19 5d830736

View on Github →

feat: IsHomeomorph predicate (#12533) Define an IsHomeomorph predicate for maps between topological spaces to complement the existing bundled Homeomorph API.

Estimated changes

Modified Mathlib/Topology/Constructions.lean

added theorem IsOpenMap.sumMap

Modified Mathlib/Topology/Homeomorph.lean

added theorem IsHomeomorph.comp

added theorem IsHomeomorph.pi_map

added theorem IsHomeomorph.prodMap

added theorem IsHomeomorph.sigmaMap

added theorem IsHomeomorph.sumMap

added structure IsHomeomorph

added theorem isHomeomorph_iff_continuous_bijective

added theorem isHomeomorph_iff_continuous_isClosedMap_bijective

added theorem isHomeomorph_iff_embedding_surjective

added theorem isHomeomorph_iff_exists_homeomorph

added theorem isHomeomorph_iff_exists_inverse

Modified Mathlib/Topology/Maps/Proper/Basic.lean

modified theorem isProperMap_id