Commit 2026-07-20 20:28 04b57243

View on Github →

feat: generalize Topology/OpenPartialHomeomorph/Basic to PartialHomeomorph (#41045) This is a continuation of #39084.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Equiv/PartialEquiv.lean

added theorem PartialEquiv.toEquiv_eq_codRestrict_restrict

added theorem PartialEquiv.toEquiv_symm_eq_codRestrict_restrict

Modified Mathlib/Topology/Constructions.lean

added theorem continuous_codRestrict_iff

Modified Mathlib/Topology/OpenPartialHomeomorph/Basic.lean

modified theorem OpenPartialHomeomorph.isOpenEmbedding_restrict

Created Mathlib/Topology/PartialHomeomorph/Basic.lean

added theorem PartialHomeomorph.coe_ofContinuousOpen

added theorem PartialHomeomorph.coe_ofContinuousOpenRestrict

added theorem PartialHomeomorph.coe_ofContinuousOpenRestrict_symm

added theorem PartialHomeomorph.coe_ofContinuousOpen_symm

added def PartialHomeomorph.homeomorphOfImageSubsetSource

added theorem PartialHomeomorph.image_eq_target_inter_inv_preimage

added theorem PartialHomeomorph.image_source_eq_target

added theorem PartialHomeomorph.image_source_inter_eq'

added theorem PartialHomeomorph.image_source_inter_eq

added theorem PartialHomeomorph.isEmbedding

added theorem PartialHomeomorph.isEmbedding_restrict

added def PartialHomeomorph.ofContinuousOpen

added def PartialHomeomorph.ofContinuousOpenRestrict

added def PartialHomeomorph.ofIsHomeomorphToEquiv

added theorem PartialHomeomorph.refl_partialEquiv

added theorem PartialHomeomorph.refl_symm

added theorem PartialHomeomorph.secondCountableTopology_source

added theorem PartialHomeomorph.source_inter_preimage_inv_preimage

added theorem PartialHomeomorph.source_inter_preimage_target_inter

added theorem PartialHomeomorph.source_preimage_target

added theorem PartialHomeomorph.symm_image_eq_source_inter_preimage

added theorem PartialHomeomorph.symm_image_target_eq_source

added theorem PartialHomeomorph.symm_image_target_inter_eq

added theorem PartialHomeomorph.target_inter_inv_preimage_preimage

added def PartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv

added def PartialHomeomorph.toHomeomorphSourceTarget

added theorem Set.partialHomeomorphSubtypeCoe_coe

added theorem Set.partialHomeomorphSubtypeCoe_source

added theorem Set.partialHomeomorphSubtypeCoe_target

added theorem Topology.IsEmbedding.toPartialHomeomorph_left_inv

added theorem Topology.IsEmbedding.toPartialHomeomorph_right_inv