Commit 2025-12-09 05:22 c186969e

View on Github →

refactor(Topology/OpenPartialHomeomorph): split long file (#32601)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Asymptotics/Lemmas.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Operations.lean

Modified Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

Modified Mathlib/Analysis/Normed/Module/Ball/Homeomorph.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/PolarCoord.lean

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

Modified Mathlib/Topology/IsLocalHomeomorph.lean

Modified Mathlib/Topology/OpenPartialHomeomorph.lean

deleted theorem Homeomorph.refl_toOpenPartialHomeomorph

deleted theorem Homeomorph.symm_toOpenPartialHomeomorph

deleted def Homeomorph.toOpenPartialHomeomorph

deleted def Homeomorph.toOpenPartialHomeomorphOfImageEq

deleted def Homeomorph.transOpenPartialHomeomorph

deleted theorem Homeomorph.transOpenPartialHomeomorph_eq_trans

deleted theorem Homeomorph.transOpenPartialHomeomorph_trans

deleted theorem Homeomorph.trans_toOpenPartialHomeomorph

deleted theorem Homeomorph.trans_transOpenPartialHomeomorph

deleted theorem OpenPartialHomeomorph.EqOnSource.eqOn

deleted theorem OpenPartialHomeomorph.EqOnSource.restr

deleted theorem OpenPartialHomeomorph.EqOnSource.source_eq

deleted theorem OpenPartialHomeomorph.EqOnSource.symm'

deleted theorem OpenPartialHomeomorph.EqOnSource.symm_eqOn_target

deleted theorem OpenPartialHomeomorph.EqOnSource.target_eq

deleted theorem OpenPartialHomeomorph.EqOnSource.trans'

deleted def OpenPartialHomeomorph.EqOnSource

deleted theorem OpenPartialHomeomorph.IsImage.apply_mem_iff

deleted theorem OpenPartialHomeomorph.IsImage.iff_preimage_eq'

deleted theorem OpenPartialHomeomorph.IsImage.iff_preimage_eq

deleted theorem OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq'

deleted theorem OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq

deleted theorem OpenPartialHomeomorph.IsImage.image_eq

deleted theorem OpenPartialHomeomorph.IsImage.inter_eq_of_inter_eq_of_eqOn

deleted theorem OpenPartialHomeomorph.IsImage.isOpen_iff

deleted theorem OpenPartialHomeomorph.IsImage.leftInvOn_piecewise

deleted theorem OpenPartialHomeomorph.IsImage.map_nhdsWithin_eq

deleted theorem OpenPartialHomeomorph.IsImage.of_image_eq

deleted theorem OpenPartialHomeomorph.IsImage.of_symm_image_eq

deleted def OpenPartialHomeomorph.IsImage.restr

deleted theorem OpenPartialHomeomorph.IsImage.symm_apply_mem_iff

deleted theorem OpenPartialHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn

deleted theorem OpenPartialHomeomorph.IsImage.symm_iff

deleted theorem OpenPartialHomeomorph.IsImage.symm_image_eq

deleted theorem OpenPartialHomeomorph.IsImage.symm_mapsTo

deleted theorem OpenPartialHomeomorph.IsImage.toPartialEquiv

deleted def OpenPartialHomeomorph.IsImage

deleted theorem OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source

deleted def OpenPartialHomeomorph.Simps.apply

deleted def OpenPartialHomeomorph.Simps.symm_apply

deleted theorem OpenPartialHomeomorph.coe_coe

deleted theorem OpenPartialHomeomorph.coe_coe_symm

deleted theorem OpenPartialHomeomorph.coe_ofContinuousOpen

deleted theorem OpenPartialHomeomorph.coe_ofContinuousOpenRestrict

deleted theorem OpenPartialHomeomorph.coe_ofContinuousOpenRestrict_symm

deleted theorem OpenPartialHomeomorph.coe_ofContinuousOpen_symm

deleted theorem OpenPartialHomeomorph.coe_restrOpen

deleted theorem OpenPartialHomeomorph.coe_restrOpen_symm

deleted theorem OpenPartialHomeomorph.coe_trans

deleted theorem OpenPartialHomeomorph.coe_trans_symm

deleted def OpenPartialHomeomorph.const

deleted theorem OpenPartialHomeomorph.const_apply

deleted theorem OpenPartialHomeomorph.const_source

deleted theorem OpenPartialHomeomorph.const_target

deleted theorem OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left

deleted theorem OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_right

deleted theorem OpenPartialHomeomorph.continuousAt_symm

deleted theorem OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_left

deleted theorem OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_right

deleted theorem OpenPartialHomeomorph.continuousOn_symm

deleted theorem OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left

deleted theorem OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right

deleted theorem OpenPartialHomeomorph.continuous_iff_continuous_comp_left

deleted def OpenPartialHomeomorph.disjointUnion

deleted theorem OpenPartialHomeomorph.eqOnSource_iff

deleted theorem OpenPartialHomeomorph.eqOnSource_refl

deleted theorem OpenPartialHomeomorph.eq_of_eqOnSource_univ

deleted theorem OpenPartialHomeomorph.eq_symm_apply

deleted theorem OpenPartialHomeomorph.eventually_left_inverse'

deleted theorem OpenPartialHomeomorph.eventually_left_inverse

deleted theorem OpenPartialHomeomorph.eventually_ne_nhdsWithin

deleted theorem OpenPartialHomeomorph.eventually_nhds'

deleted theorem OpenPartialHomeomorph.eventually_nhds

deleted theorem OpenPartialHomeomorph.eventually_nhdsWithin'

deleted theorem OpenPartialHomeomorph.eventually_nhdsWithin

deleted theorem OpenPartialHomeomorph.eventually_right_inverse'

deleted theorem OpenPartialHomeomorph.eventually_right_inverse

deleted def OpenPartialHomeomorph.homeomorphOfImageSubsetSource

deleted theorem OpenPartialHomeomorph.image_eq_target_inter_inv_preimage

deleted theorem OpenPartialHomeomorph.image_mem_nhds

deleted theorem OpenPartialHomeomorph.image_source_eq_target

deleted theorem OpenPartialHomeomorph.image_source_inter_eq'

deleted theorem OpenPartialHomeomorph.image_source_inter_eq

deleted theorem OpenPartialHomeomorph.image_trans_source

deleted theorem OpenPartialHomeomorph.invFun_eq_coe

deleted theorem OpenPartialHomeomorph.inv_image_trans_target

deleted theorem OpenPartialHomeomorph.isImage_source_target

deleted theorem OpenPartialHomeomorph.isImage_source_target_of_disjoint

deleted theorem OpenPartialHomeomorph.isOpenEmbedding_restrict

deleted theorem OpenPartialHomeomorph.isOpen_image_iff_of_subset_source

deleted theorem OpenPartialHomeomorph.isOpen_image_of_subset_source

deleted theorem OpenPartialHomeomorph.isOpen_image_source_inter

deleted theorem OpenPartialHomeomorph.isOpen_image_symm_of_subset_target

deleted theorem OpenPartialHomeomorph.isOpen_inter_preimage

deleted theorem OpenPartialHomeomorph.isOpen_inter_preimage_symm

deleted theorem OpenPartialHomeomorph.isOpen_symm_image_iff_of_subset_target

deleted theorem OpenPartialHomeomorph.left_inv

deleted theorem OpenPartialHomeomorph.lift_openEmbedding_apply

deleted theorem OpenPartialHomeomorph.lift_openEmbedding_source

deleted theorem OpenPartialHomeomorph.lift_openEmbedding_symm

deleted theorem OpenPartialHomeomorph.lift_openEmbedding_symm_source

deleted theorem OpenPartialHomeomorph.lift_openEmbedding_symm_target

deleted theorem OpenPartialHomeomorph.lift_openEmbedding_target

deleted theorem OpenPartialHomeomorph.lift_openEmbedding_toFun

deleted theorem OpenPartialHomeomorph.lift_openEmbedding_trans

deleted theorem OpenPartialHomeomorph.lift_openEmbedding_trans_apply

deleted theorem OpenPartialHomeomorph.map_nhdsWithin_eq

deleted theorem OpenPartialHomeomorph.map_nhdsWithin_preimage_eq

deleted theorem OpenPartialHomeomorph.map_nhds_eq

deleted theorem OpenPartialHomeomorph.map_source''

deleted theorem OpenPartialHomeomorph.map_source

deleted theorem OpenPartialHomeomorph.map_subtype_source

deleted theorem OpenPartialHomeomorph.map_target

deleted theorem OpenPartialHomeomorph.mk_coe

deleted theorem OpenPartialHomeomorph.mk_coe_symm

deleted theorem OpenPartialHomeomorph.nhdsWithin_source_inter

deleted theorem OpenPartialHomeomorph.nhdsWithin_target_inter

deleted theorem OpenPartialHomeomorph.nhds_eq_comap_inf_principal

deleted def OpenPartialHomeomorph.ofContinuousOpen

deleted def OpenPartialHomeomorph.ofContinuousOpenRestrict

deleted def OpenPartialHomeomorph.ofSet

deleted theorem OpenPartialHomeomorph.ofSet_symm

deleted theorem OpenPartialHomeomorph.ofSet_toPartialEquiv

deleted theorem OpenPartialHomeomorph.ofSet_trans'

deleted theorem OpenPartialHomeomorph.ofSet_trans

deleted theorem OpenPartialHomeomorph.ofSet_trans_ofSet

deleted theorem OpenPartialHomeomorph.ofSet_univ_eq_refl

deleted def OpenPartialHomeomorph.pi

deleted def OpenPartialHomeomorph.piecewise

deleted theorem OpenPartialHomeomorph.preimage_closure

deleted theorem OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter

deleted theorem OpenPartialHomeomorph.preimage_frontier

deleted theorem OpenPartialHomeomorph.preimage_interior

deleted def OpenPartialHomeomorph.prod

deleted theorem OpenPartialHomeomorph.prod_eq_prod_of_nonempty'

deleted theorem OpenPartialHomeomorph.prod_eq_prod_of_nonempty

deleted theorem OpenPartialHomeomorph.prod_symm

deleted theorem OpenPartialHomeomorph.prod_trans

deleted theorem OpenPartialHomeomorph.refl_partialEquiv

deleted theorem OpenPartialHomeomorph.refl_prod_refl

deleted theorem OpenPartialHomeomorph.refl_symm

deleted theorem OpenPartialHomeomorph.refl_trans

deleted def OpenPartialHomeomorph.replaceEquiv

deleted theorem OpenPartialHomeomorph.replaceEquiv_eq_self

deleted theorem OpenPartialHomeomorph.restrOpen_source

deleted theorem OpenPartialHomeomorph.restrOpen_toPartialEquiv

deleted theorem OpenPartialHomeomorph.restr_eqOnSource_restr

deleted theorem OpenPartialHomeomorph.restr_eq_of_source_subset

deleted theorem OpenPartialHomeomorph.restr_inter_source

deleted theorem OpenPartialHomeomorph.restr_source'

deleted theorem OpenPartialHomeomorph.restr_source_inter

deleted theorem OpenPartialHomeomorph.restr_symm_trans

deleted theorem OpenPartialHomeomorph.restr_toPartialEquiv'

deleted theorem OpenPartialHomeomorph.restr_toPartialEquiv

deleted theorem OpenPartialHomeomorph.restr_trans

deleted theorem OpenPartialHomeomorph.restr_univ

deleted theorem OpenPartialHomeomorph.right_inv

deleted theorem OpenPartialHomeomorph.secondCountableTopology_source

deleted theorem OpenPartialHomeomorph.self_trans_symm

deleted theorem OpenPartialHomeomorph.source_inter_preimage_inv_preimage

deleted theorem OpenPartialHomeomorph.source_inter_preimage_target_inter

deleted theorem OpenPartialHomeomorph.source_preimage_target

deleted theorem OpenPartialHomeomorph.subtypeRestr_coe

deleted theorem OpenPartialHomeomorph.subtypeRestr_def

deleted theorem OpenPartialHomeomorph.subtypeRestr_source

deleted theorem OpenPartialHomeomorph.subtypeRestr_symm_eqOn

deleted theorem OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le

deleted theorem OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr

deleted theorem OpenPartialHomeomorph.symm_bijective

deleted theorem OpenPartialHomeomorph.symm_image_eq_source_inter_preimage

deleted theorem OpenPartialHomeomorph.symm_image_target_eq_source

deleted theorem OpenPartialHomeomorph.symm_image_target_inter_eq

deleted theorem OpenPartialHomeomorph.symm_map_nhds_eq

deleted theorem OpenPartialHomeomorph.symm_piecewise

deleted theorem OpenPartialHomeomorph.symm_source

deleted theorem OpenPartialHomeomorph.symm_symm

deleted theorem OpenPartialHomeomorph.symm_target

deleted theorem OpenPartialHomeomorph.symm_toPartialEquiv

deleted theorem OpenPartialHomeomorph.symm_trans_restr

deleted theorem OpenPartialHomeomorph.symm_trans_self

deleted theorem OpenPartialHomeomorph.target_inter_inv_preimage_preimage

deleted theorem OpenPartialHomeomorph.tendsto_symm

deleted def OpenPartialHomeomorph.toFun'

deleted theorem OpenPartialHomeomorph.toFun_eq_coe

deleted def OpenPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv

deleted def OpenPartialHomeomorph.toHomeomorphSourceTarget

deleted theorem OpenPartialHomeomorph.toPartialEquiv_injective

deleted theorem OpenPartialHomeomorph.to_isOpenEmbedding

deleted def OpenPartialHomeomorph.transHomeomorph

deleted theorem OpenPartialHomeomorph.transHomeomorph_eq_trans

deleted theorem OpenPartialHomeomorph.transHomeomorph_transHomeomorph

deleted theorem OpenPartialHomeomorph.trans_apply

deleted theorem OpenPartialHomeomorph.trans_assoc

deleted theorem OpenPartialHomeomorph.trans_ofSet

deleted theorem OpenPartialHomeomorph.trans_of_set'

deleted theorem OpenPartialHomeomorph.trans_refl

deleted theorem OpenPartialHomeomorph.trans_source''

deleted theorem OpenPartialHomeomorph.trans_source'

deleted theorem OpenPartialHomeomorph.trans_source

deleted theorem OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm

deleted theorem OpenPartialHomeomorph.trans_target''

deleted theorem OpenPartialHomeomorph.trans_target'

deleted theorem OpenPartialHomeomorph.trans_target

deleted theorem OpenPartialHomeomorph.trans_toPartialEquiv

deleted theorem OpenPartialHomeomorph.trans_transHomeomorph

deleted structure OpenPartialHomeomorph

deleted theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_coe

deleted theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_source

deleted theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target

deleted theorem Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv

deleted theorem Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv

Created Mathlib/Topology/OpenPartialHomeomorph/Basic.lean

added theorem OpenPartialHomeomorph.coe_ofContinuousOpen

added theorem OpenPartialHomeomorph.coe_ofContinuousOpenRestrict

added theorem OpenPartialHomeomorph.coe_ofContinuousOpenRestrict_symm

added theorem OpenPartialHomeomorph.coe_ofContinuousOpen_symm

added def OpenPartialHomeomorph.homeomorphOfImageSubsetSource

added theorem OpenPartialHomeomorph.image_eq_target_inter_inv_preimage

added theorem OpenPartialHomeomorph.image_source_eq_target

added theorem OpenPartialHomeomorph.image_source_inter_eq'

added theorem OpenPartialHomeomorph.image_source_inter_eq

added theorem OpenPartialHomeomorph.isOpenEmbedding_restrict

added theorem OpenPartialHomeomorph.isOpen_image_iff_of_subset_source

added theorem OpenPartialHomeomorph.isOpen_image_of_subset_source

added theorem OpenPartialHomeomorph.isOpen_image_source_inter

added theorem OpenPartialHomeomorph.isOpen_image_symm_of_subset_target

added theorem OpenPartialHomeomorph.isOpen_inter_preimage

added theorem OpenPartialHomeomorph.isOpen_inter_preimage_symm

added theorem OpenPartialHomeomorph.isOpen_symm_image_iff_of_subset_target

added theorem OpenPartialHomeomorph.nhds_eq_comap_inf_principal

added def OpenPartialHomeomorph.ofContinuousOpen

added def OpenPartialHomeomorph.ofContinuousOpenRestrict

added theorem OpenPartialHomeomorph.refl_partialEquiv

added theorem OpenPartialHomeomorph.refl_symm

added theorem OpenPartialHomeomorph.secondCountableTopology_source

added theorem OpenPartialHomeomorph.source_inter_preimage_inv_preimage

added theorem OpenPartialHomeomorph.source_inter_preimage_target_inter

added theorem OpenPartialHomeomorph.source_preimage_target

added theorem OpenPartialHomeomorph.symm_image_eq_source_inter_preimage

added theorem OpenPartialHomeomorph.symm_image_target_eq_source

added theorem OpenPartialHomeomorph.symm_image_target_inter_eq

added theorem OpenPartialHomeomorph.target_inter_inv_preimage_preimage

added def OpenPartialHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv

added def OpenPartialHomeomorph.toHomeomorphSourceTarget

added theorem OpenPartialHomeomorph.to_isOpenEmbedding

added theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_coe

added theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_source

added theorem TopologicalSpace.Opens.openPartialHomeomorphSubtypeCoe_target

added theorem Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv

added theorem Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv

Created Mathlib/Topology/OpenPartialHomeomorph/Composition.lean

added def Homeomorph.transOpenPartialHomeomorph

added theorem Homeomorph.transOpenPartialHomeomorph_eq_trans

added theorem Homeomorph.transOpenPartialHomeomorph_trans

added theorem Homeomorph.trans_toOpenPartialHomeomorph

added theorem Homeomorph.trans_transOpenPartialHomeomorph

added theorem OpenPartialHomeomorph.EqOnSource.trans'

added theorem OpenPartialHomeomorph.coe_trans

added theorem OpenPartialHomeomorph.coe_trans_symm

added theorem OpenPartialHomeomorph.image_trans_source

added theorem OpenPartialHomeomorph.inv_image_trans_target

added theorem OpenPartialHomeomorph.ofSet_trans'

added theorem OpenPartialHomeomorph.ofSet_trans

added theorem OpenPartialHomeomorph.ofSet_trans_ofSet

added theorem OpenPartialHomeomorph.refl_trans

added theorem OpenPartialHomeomorph.restr_symm_trans

added theorem OpenPartialHomeomorph.restr_trans

added theorem OpenPartialHomeomorph.self_trans_symm

added theorem OpenPartialHomeomorph.symm_trans_restr

added theorem OpenPartialHomeomorph.symm_trans_self

added theorem OpenPartialHomeomorph.trans_apply

added theorem OpenPartialHomeomorph.trans_assoc

added theorem OpenPartialHomeomorph.trans_ofSet

added theorem OpenPartialHomeomorph.trans_of_set'

added theorem OpenPartialHomeomorph.trans_refl

added theorem OpenPartialHomeomorph.trans_source''

added theorem OpenPartialHomeomorph.trans_source'

added theorem OpenPartialHomeomorph.trans_source

added theorem OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm

added theorem OpenPartialHomeomorph.trans_target''

added theorem OpenPartialHomeomorph.trans_target'

added theorem OpenPartialHomeomorph.trans_target

added theorem OpenPartialHomeomorph.trans_toPartialEquiv

Created Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean

added def OpenPartialHomeomorph.const

added theorem OpenPartialHomeomorph.const_apply

added theorem OpenPartialHomeomorph.const_source

added theorem OpenPartialHomeomorph.const_target

added def OpenPartialHomeomorph.disjointUnion

added theorem OpenPartialHomeomorph.lift_openEmbedding_apply

added theorem OpenPartialHomeomorph.lift_openEmbedding_source

added theorem OpenPartialHomeomorph.lift_openEmbedding_symm

added theorem OpenPartialHomeomorph.lift_openEmbedding_symm_source

added theorem OpenPartialHomeomorph.lift_openEmbedding_symm_target

added theorem OpenPartialHomeomorph.lift_openEmbedding_target

added theorem OpenPartialHomeomorph.lift_openEmbedding_toFun

added theorem OpenPartialHomeomorph.lift_openEmbedding_trans

added theorem OpenPartialHomeomorph.lift_openEmbedding_trans_apply

added theorem OpenPartialHomeomorph.map_subtype_source

added def OpenPartialHomeomorph.pi

added def OpenPartialHomeomorph.piecewise

added def OpenPartialHomeomorph.prod

added theorem OpenPartialHomeomorph.prod_eq_prod_of_nonempty'

added theorem OpenPartialHomeomorph.prod_eq_prod_of_nonempty

added theorem OpenPartialHomeomorph.prod_symm

added theorem OpenPartialHomeomorph.prod_trans

added theorem OpenPartialHomeomorph.refl_prod_refl

added theorem OpenPartialHomeomorph.subtypeRestr_coe

added theorem OpenPartialHomeomorph.subtypeRestr_def

added theorem OpenPartialHomeomorph.subtypeRestr_source

added theorem OpenPartialHomeomorph.subtypeRestr_symm_eqOn

added theorem OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le

added theorem OpenPartialHomeomorph.subtypeRestr_symm_trans_subtypeRestr

added theorem OpenPartialHomeomorph.symm_piecewise

added def OpenPartialHomeomorph.transHomeomorph

added theorem OpenPartialHomeomorph.transHomeomorph_eq_trans

added theorem OpenPartialHomeomorph.transHomeomorph_transHomeomorph

added theorem OpenPartialHomeomorph.trans_transHomeomorph

Created Mathlib/Topology/OpenPartialHomeomorph/Continuity.lean

added theorem OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left

added theorem OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_right

added theorem OpenPartialHomeomorph.continuousAt_symm

added theorem OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_left

added theorem OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_right

added theorem OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left

added theorem OpenPartialHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right

added theorem OpenPartialHomeomorph.continuous_iff_continuous_comp_left

added theorem OpenPartialHomeomorph.eventually_left_inverse'

added theorem OpenPartialHomeomorph.eventually_left_inverse

added theorem OpenPartialHomeomorph.eventually_ne_nhdsWithin

added theorem OpenPartialHomeomorph.eventually_nhds'

added theorem OpenPartialHomeomorph.eventually_nhds

added theorem OpenPartialHomeomorph.eventually_nhdsWithin'

added theorem OpenPartialHomeomorph.eventually_nhdsWithin

added theorem OpenPartialHomeomorph.eventually_right_inverse'

added theorem OpenPartialHomeomorph.eventually_right_inverse

added theorem OpenPartialHomeomorph.image_mem_nhds

added theorem OpenPartialHomeomorph.map_nhdsWithin_eq

added theorem OpenPartialHomeomorph.map_nhdsWithin_preimage_eq

added theorem OpenPartialHomeomorph.map_nhds_eq

added theorem OpenPartialHomeomorph.nhdsWithin_source_inter

added theorem OpenPartialHomeomorph.nhdsWithin_target_inter

added theorem OpenPartialHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter

added theorem OpenPartialHomeomorph.symm_map_nhds_eq

added theorem OpenPartialHomeomorph.tendsto_symm

Created Mathlib/Topology/OpenPartialHomeomorph/Defs.lean

added def Homeomorph.toOpenPartialHomeomorph

added def Homeomorph.toOpenPartialHomeomorphOfImageEq

added def OpenPartialHomeomorph.Simps.apply

added def OpenPartialHomeomorph.Simps.symm_apply

added theorem OpenPartialHomeomorph.coe_coe

added theorem OpenPartialHomeomorph.coe_coe_symm

added theorem OpenPartialHomeomorph.continuousOn_symm

added theorem OpenPartialHomeomorph.eq_symm_apply

added theorem OpenPartialHomeomorph.invFun_eq_coe

added theorem OpenPartialHomeomorph.left_inv

added theorem OpenPartialHomeomorph.map_source''

added theorem OpenPartialHomeomorph.map_source

added theorem OpenPartialHomeomorph.map_target

added theorem OpenPartialHomeomorph.mk_coe

added theorem OpenPartialHomeomorph.mk_coe_symm

added def OpenPartialHomeomorph.replaceEquiv

added theorem OpenPartialHomeomorph.replaceEquiv_eq_self

added theorem OpenPartialHomeomorph.right_inv

added theorem OpenPartialHomeomorph.symm_bijective

added theorem OpenPartialHomeomorph.symm_source

added theorem OpenPartialHomeomorph.symm_symm

added theorem OpenPartialHomeomorph.symm_target

added theorem OpenPartialHomeomorph.symm_toPartialEquiv

added def OpenPartialHomeomorph.toFun'

added theorem OpenPartialHomeomorph.toFun_eq_coe

added theorem OpenPartialHomeomorph.toPartialEquiv_injective

added structure OpenPartialHomeomorph

Created Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean

added theorem Homeomorph.refl_toOpenPartialHomeomorph

added theorem Homeomorph.symm_toOpenPartialHomeomorph

added theorem OpenPartialHomeomorph.EqOnSource.eqOn

added theorem OpenPartialHomeomorph.EqOnSource.restr

added theorem OpenPartialHomeomorph.EqOnSource.source_eq

added theorem OpenPartialHomeomorph.EqOnSource.symm'

added theorem OpenPartialHomeomorph.EqOnSource.symm_eqOn_target

added theorem OpenPartialHomeomorph.EqOnSource.target_eq

added def OpenPartialHomeomorph.EqOnSource

added theorem OpenPartialHomeomorph.IsImage.apply_mem_iff

added theorem OpenPartialHomeomorph.IsImage.iff_preimage_eq'

added theorem OpenPartialHomeomorph.IsImage.iff_preimage_eq

added theorem OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq'

added theorem OpenPartialHomeomorph.IsImage.iff_symm_preimage_eq

added theorem OpenPartialHomeomorph.IsImage.image_eq

added theorem OpenPartialHomeomorph.IsImage.inter_eq_of_inter_eq_of_eqOn

added theorem OpenPartialHomeomorph.IsImage.isOpen_iff

added theorem OpenPartialHomeomorph.IsImage.leftInvOn_piecewise

added theorem OpenPartialHomeomorph.IsImage.map_nhdsWithin_eq

added theorem OpenPartialHomeomorph.IsImage.of_image_eq

added theorem OpenPartialHomeomorph.IsImage.of_symm_image_eq

added def OpenPartialHomeomorph.IsImage.restr

added theorem OpenPartialHomeomorph.IsImage.symm_apply_mem_iff

added theorem OpenPartialHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn

added theorem OpenPartialHomeomorph.IsImage.symm_iff

added theorem OpenPartialHomeomorph.IsImage.symm_image_eq

added theorem OpenPartialHomeomorph.IsImage.symm_mapsTo

added theorem OpenPartialHomeomorph.IsImage.toPartialEquiv

added def OpenPartialHomeomorph.IsImage

added theorem OpenPartialHomeomorph.Set.EqOn.restr_eqOn_source

added theorem OpenPartialHomeomorph.coe_restrOpen

added theorem OpenPartialHomeomorph.coe_restrOpen_symm

added theorem OpenPartialHomeomorph.eqOnSource_iff

added theorem OpenPartialHomeomorph.eqOnSource_refl

added theorem OpenPartialHomeomorph.eq_of_eqOnSource_univ

added theorem OpenPartialHomeomorph.isImage_source_target

added theorem OpenPartialHomeomorph.isImage_source_target_of_disjoint

added def OpenPartialHomeomorph.ofSet

added theorem OpenPartialHomeomorph.ofSet_symm

added theorem OpenPartialHomeomorph.ofSet_toPartialEquiv

added theorem OpenPartialHomeomorph.ofSet_univ_eq_refl

added theorem OpenPartialHomeomorph.preimage_closure

added theorem OpenPartialHomeomorph.preimage_frontier

added theorem OpenPartialHomeomorph.preimage_interior

added theorem OpenPartialHomeomorph.restrOpen_source

added theorem OpenPartialHomeomorph.restrOpen_toPartialEquiv

added theorem OpenPartialHomeomorph.restr_eqOnSource_restr

added theorem OpenPartialHomeomorph.restr_eq_of_source_subset

added theorem OpenPartialHomeomorph.restr_inter_source

added theorem OpenPartialHomeomorph.restr_source'

added theorem OpenPartialHomeomorph.restr_source_inter

added theorem OpenPartialHomeomorph.restr_toPartialEquiv'

added theorem OpenPartialHomeomorph.restr_toPartialEquiv

added theorem OpenPartialHomeomorph.restr_univ