Commit 2023-02-18 19:03 2f7cbdca

View on Github →

feat: port Topology.LocalHomeomorph (#2231)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Equiv/LocalEquiv.lean

added theorem LocalEquiv.trans_ofSet

Created Mathlib/Topology/LocalHomeomorph.lean

added theorem Homeomorph.refl_toLocalHomeomorph

added theorem Homeomorph.symm_toLocalHomeomorph

added def Homeomorph.toLocalHomeomorph

added def Homeomorph.transLocalHomeomorph

added theorem Homeomorph.transLocalHomeomorph_eq_trans

added theorem Homeomorph.trans_toLocalHomeomorph

added theorem LocalHomeomorph.EqOnSource.eqOn

added theorem LocalHomeomorph.EqOnSource.restr

added theorem LocalHomeomorph.EqOnSource.source_eq

added theorem LocalHomeomorph.EqOnSource.symm'

added theorem LocalHomeomorph.EqOnSource.symm_eqOn_target

added theorem LocalHomeomorph.EqOnSource.target_eq

added theorem LocalHomeomorph.EqOnSource.trans'

added def LocalHomeomorph.EqOnSource

added theorem LocalHomeomorph.IsImage.apply_mem_iff

added theorem LocalHomeomorph.IsImage.iff_preimage_eq'

added theorem LocalHomeomorph.IsImage.iff_preimage_eq

added theorem LocalHomeomorph.IsImage.iff_symm_preimage_eq'

added theorem LocalHomeomorph.IsImage.iff_symm_preimage_eq

added theorem LocalHomeomorph.IsImage.image_eq

added theorem LocalHomeomorph.IsImage.inter_eq_of_inter_eq_of_eqOn

added theorem LocalHomeomorph.IsImage.isOpen_iff

added theorem LocalHomeomorph.IsImage.leftInvOn_piecewise

added theorem LocalHomeomorph.IsImage.map_nhdsWithin_eq

added theorem LocalHomeomorph.IsImage.of_image_eq

added theorem LocalHomeomorph.IsImage.of_symm_image_eq

added def LocalHomeomorph.IsImage.restr

added theorem LocalHomeomorph.IsImage.symm_apply_mem_iff

added theorem LocalHomeomorph.IsImage.symm_eqOn_of_inter_eq_of_eqOn

added theorem LocalHomeomorph.IsImage.symm_iff

added theorem LocalHomeomorph.IsImage.symm_image_eq

added theorem LocalHomeomorph.IsImage.symm_mapsTo

added theorem LocalHomeomorph.IsImage.toLocalEquiv

added def LocalHomeomorph.IsImage

added theorem LocalHomeomorph.Set.EqOn.restr_eqOn_source

added def LocalHomeomorph.Simps.apply

added def LocalHomeomorph.Simps.symm_apply

added theorem LocalHomeomorph.coe_coe

added theorem LocalHomeomorph.coe_coe_symm

added theorem LocalHomeomorph.coe_trans

added theorem LocalHomeomorph.coe_trans_symm

added theorem LocalHomeomorph.continuousAt_iff_continuousAt_comp_left

added theorem LocalHomeomorph.continuousAt_iff_continuousAt_comp_right

added theorem LocalHomeomorph.continuousAt_symm

added theorem LocalHomeomorph.continuousOn_iff_continuousOn_comp_left

added theorem LocalHomeomorph.continuousOn_iff_continuousOn_comp_right

added theorem LocalHomeomorph.continuousOn_symm

added theorem LocalHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_left

added theorem LocalHomeomorph.continuousWithinAt_iff_continuousWithinAt_comp_right

added theorem LocalHomeomorph.continuous_iff_continuous_comp_left

added def LocalHomeomorph.disjointUnion

added theorem LocalHomeomorph.eqOnSource_iff

added theorem LocalHomeomorph.eqOnSource_refl

added theorem LocalHomeomorph.eq_of_eq_on_source_univ

added theorem LocalHomeomorph.eq_of_localEquiv_eq

added theorem LocalHomeomorph.eq_symm_apply

added theorem LocalHomeomorph.eventually_left_inverse'

added theorem LocalHomeomorph.eventually_left_inverse

added theorem LocalHomeomorph.eventually_ne_nhdsWithin

added theorem LocalHomeomorph.eventually_nhds'

added theorem LocalHomeomorph.eventually_nhds

added theorem LocalHomeomorph.eventually_nhdsWithin'

added theorem LocalHomeomorph.eventually_nhdsWithin

added theorem LocalHomeomorph.eventually_right_inverse'

added theorem LocalHomeomorph.eventually_right_inverse

added def LocalHomeomorph.homeomorphOfImageSubsetSource

added theorem LocalHomeomorph.image_eq_target_inter_inv_preimage

added theorem LocalHomeomorph.image_mem_nhds

added theorem LocalHomeomorph.image_open_of_open'

added theorem LocalHomeomorph.image_open_of_open

added theorem LocalHomeomorph.image_source_eq_target

added theorem LocalHomeomorph.image_source_inter_eq'

added theorem LocalHomeomorph.image_source_inter_eq

added theorem LocalHomeomorph.image_trans_source

added theorem LocalHomeomorph.invFun_eq_coe

added theorem LocalHomeomorph.inv_image_trans_target

added theorem LocalHomeomorph.isImage_source_target

added theorem LocalHomeomorph.isImage_source_target_of_disjoint

added theorem LocalHomeomorph.left_inv

added theorem LocalHomeomorph.map_nhdsWithin_eq

added theorem LocalHomeomorph.map_nhdsWithin_preimage_eq

added theorem LocalHomeomorph.map_nhds_eq

added theorem LocalHomeomorph.map_source

added theorem LocalHomeomorph.map_target

added theorem LocalHomeomorph.mk_coe

added theorem LocalHomeomorph.mk_coe_symm

added theorem LocalHomeomorph.nhdsWithin_source_inter

added theorem LocalHomeomorph.nhdsWithin_target_inter

added def LocalHomeomorph.ofContinuousOpen

added def LocalHomeomorph.ofContinuousOpenRestrict

added def LocalHomeomorph.ofSet

added theorem LocalHomeomorph.ofSet_symm

added theorem LocalHomeomorph.ofSet_toLocalEquiv

added theorem LocalHomeomorph.ofSet_trans'

added theorem LocalHomeomorph.ofSet_trans

added theorem LocalHomeomorph.ofSet_trans_ofSet

added theorem LocalHomeomorph.ofSet_univ_eq_refl

added def LocalHomeomorph.pi

added def LocalHomeomorph.piecewise

added theorem LocalHomeomorph.preimage_closure

added theorem LocalHomeomorph.preimage_eventuallyEq_target_inter_preimage_inter

added theorem LocalHomeomorph.preimage_frontier

added theorem LocalHomeomorph.preimage_interior

added theorem LocalHomeomorph.preimage_open_of_open

added theorem LocalHomeomorph.preimage_open_of_open_symm

added def LocalHomeomorph.prod

added theorem LocalHomeomorph.prod_eq_prod_of_nonempty'

added theorem LocalHomeomorph.prod_eq_prod_of_nonempty

added theorem LocalHomeomorph.prod_symm

added theorem LocalHomeomorph.prod_trans

added theorem LocalHomeomorph.refl_localEquiv

added theorem LocalHomeomorph.refl_prod_refl

added theorem LocalHomeomorph.refl_symm

added theorem LocalHomeomorph.refl_trans

added def LocalHomeomorph.replaceEquiv

added theorem LocalHomeomorph.replaceEquiv_eq_self

added theorem LocalHomeomorph.restrOpen_source

added theorem LocalHomeomorph.restrOpen_toLocalEquiv

added theorem LocalHomeomorph.restr_eq_of_source_subset

added theorem LocalHomeomorph.restr_source'

added theorem LocalHomeomorph.restr_source_inter

added theorem LocalHomeomorph.restr_toLocalEquiv'

added theorem LocalHomeomorph.restr_toLocalEquiv

added theorem LocalHomeomorph.restr_trans

added theorem LocalHomeomorph.restr_univ

added theorem LocalHomeomorph.right_inv

added theorem LocalHomeomorph.secondCountableTopology_source

added theorem LocalHomeomorph.source_inter_preimage_inv_preimage

added theorem LocalHomeomorph.source_inter_preimage_target_inter

added theorem LocalHomeomorph.source_preimage_target

added theorem LocalHomeomorph.subtypeRestr_coe

added theorem LocalHomeomorph.subtypeRestr_def

added theorem LocalHomeomorph.subtypeRestr_source

added theorem LocalHomeomorph.subtypeRestr_symm_trans_subtypeRestr

added theorem LocalHomeomorph.symm_image_eq_source_inter_preimage

added theorem LocalHomeomorph.symm_image_target_eq_source

added theorem LocalHomeomorph.symm_image_target_inter_eq

added theorem LocalHomeomorph.symm_map_nhds_eq

added theorem LocalHomeomorph.symm_piecewise

added theorem LocalHomeomorph.symm_source

added theorem LocalHomeomorph.symm_symm

added theorem LocalHomeomorph.symm_target

added theorem LocalHomeomorph.symm_toLocalEquiv

added theorem LocalHomeomorph.target_inter_inv_preimage_preimage

added theorem LocalHomeomorph.tendsto_symm

added def LocalHomeomorph.toFun'

added theorem LocalHomeomorph.toFun_eq_coe

added def LocalHomeomorph.toHomeomorphOfSourceEqUnivTargetEqUniv

added def LocalHomeomorph.toHomeomorphSourceTarget

added theorem LocalHomeomorph.toLocalEquiv_injective

added theorem LocalHomeomorph.to_openEmbedding

added def LocalHomeomorph.transHomeomorph

added theorem LocalHomeomorph.trans_apply

added theorem LocalHomeomorph.trans_assoc

added theorem LocalHomeomorph.trans_equiv_eq_trans

added theorem LocalHomeomorph.trans_ofSet

added theorem LocalHomeomorph.trans_of_set'

added theorem LocalHomeomorph.trans_refl

added theorem LocalHomeomorph.trans_self_symm

added theorem LocalHomeomorph.trans_source''

added theorem LocalHomeomorph.trans_source'

added theorem LocalHomeomorph.trans_source

added theorem LocalHomeomorph.trans_symm_eq_symm_trans_symm

added theorem LocalHomeomorph.trans_symm_self

added theorem LocalHomeomorph.trans_target''

added theorem LocalHomeomorph.trans_target'

added theorem LocalHomeomorph.trans_target

added theorem LocalHomeomorph.trans_toLocalEquiv

added structure LocalHomeomorph

added theorem OpenEmbedding.continuousAt_iff

added theorem TopologicalSpace.Opens.localHomeomorphSubtypeCoe_coe

added theorem TopologicalSpace.Opens.localHomeomorphSubtypeCoe_source

added theorem TopologicalSpace.Opens.localHomeomorphSubtypeCoe_target

Modified Mathlib/Topology/Maps.lean

added theorem OpenEmbedding.tendsto_nhds_iff'