Commit 2023-02-02 14:55 df324206

View on Github →

feat: port Topology.Homeomorph (#2004)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Homeomorph.lean

added theorem Continuous.continuous_symm_of_equiv_compact_to_t2

added def Continuous.homeoOfEquivCompactToT2

added def Equiv.toHomeomorphOfInducing

added theorem HasCompactMulSupport.comp_homeomorph

added def Homeomorph.Set.prod

added def Homeomorph.Set.univ

added def Homeomorph.Simps.apply

added def Homeomorph.Simps.symm_apply

added theorem Homeomorph.apply_symm_apply

added def Homeomorph.changeInv

added theorem Homeomorph.coe_prodComm

added theorem Homeomorph.coe_prodCongr

added theorem Homeomorph.coe_punitProd

added theorem Homeomorph.coe_symm_toEquiv

added theorem Homeomorph.coe_toEquiv

added theorem Homeomorph.coinduced_eq

added theorem Homeomorph.comap_cocompact

added theorem Homeomorph.comap_nhds_eq

added theorem Homeomorph.comp_continuousAt_iff'

added theorem Homeomorph.comp_continuousAt_iff

added theorem Homeomorph.comp_continuousOn_iff

added theorem Homeomorph.comp_continuousWithinAt_iff

added theorem Homeomorph.comp_continuous_iff'

added theorem Homeomorph.comp_continuous_iff

added theorem Homeomorph.comp_isOpenMap_iff'

added theorem Homeomorph.comp_isOpenMap_iff

added theorem Homeomorph.ext

added def Homeomorph.finTwoArrow

added def Homeomorph.funSplitAt

added def Homeomorph.funUnique

added def Homeomorph.homeomorphOfContinuousOpen

added def Homeomorph.homeomorphOfUnique

added theorem Homeomorph.homeomorph_mk_coe

added theorem Homeomorph.homeomorph_mk_coe_symm

added def Homeomorph.image

added theorem Homeomorph.image_closure

added theorem Homeomorph.image_frontier

added theorem Homeomorph.image_interior

added theorem Homeomorph.image_preimage

added theorem Homeomorph.image_symm

added theorem Homeomorph.induced_eq

added theorem Homeomorph.isClosed_image

added theorem Homeomorph.isClosed_preimage

added theorem Homeomorph.isCompact_image

added theorem Homeomorph.isCompact_preimage

added theorem Homeomorph.isOpen_image

added theorem Homeomorph.isOpen_preimage

added theorem Homeomorph.map_cocompact

added theorem Homeomorph.map_nhds_eq

added theorem Homeomorph.nhds_eq_comap

added def Homeomorph.piCongrRight

added theorem Homeomorph.piCongrRight_symm

added def Homeomorph.piEquivPiSubtypeProd

added def Homeomorph.piFinTwo.{u}

added def Homeomorph.piSplitAt

added theorem Homeomorph.preimage_closure

added theorem Homeomorph.preimage_frontier

added theorem Homeomorph.preimage_image

added theorem Homeomorph.preimage_interior

added theorem Homeomorph.preimage_symm

added def Homeomorph.prodAssoc

added def Homeomorph.prodComm

added theorem Homeomorph.prodComm_symm

added def Homeomorph.prodCongr

added theorem Homeomorph.prodCongr_symm

added def Homeomorph.prodPunit

added def Homeomorph.prodSumDistrib

added def Homeomorph.punitProd

added theorem Homeomorph.range_coe

added theorem Homeomorph.refl_symm

added theorem Homeomorph.self_comp_symm

added theorem Homeomorph.self_trans_symm

added def Homeomorph.setCongr

added def Homeomorph.sigmaProdDistrib

added def Homeomorph.sumCongr

added def Homeomorph.sumProdDistrib

added theorem Homeomorph.symm_apply_apply

added theorem Homeomorph.symm_comp_self

added theorem Homeomorph.symm_map_nhds_eq

added theorem Homeomorph.symm_trans_self

added theorem Homeomorph.toEquiv_injective

added theorem Homeomorph.trans_apply

added def Homeomorph.ulift.{u,

added structure Homeomorph