Commit 2023-10-11 19:02 b39fc2a8

View on Github →

chore(Topology/Homeomorph): rename type variables (#7587) X, Y, Z are standard mathematical names for topological spaces. As discussed on zulip, let us rename them.

Estimated changes

Modified Mathlib/Topology/Homeomorph.lean

modified theorem Continuous.continuous_symm_of_equiv_compact_to_t2

modified def Continuous.homeoOfEquivCompactToT2

modified theorem Equiv.coe_toHomeomorph

modified def Equiv.toHomeomorph

modified def Equiv.toHomeomorphOfInducing

modified theorem Equiv.toHomeomorph_apply

modified theorem Equiv.toHomeomorph_symm

modified theorem Equiv.toHomeomorph_trans

modified theorem HasCompactMulSupport.comp_homeomorph

modified def Homeomorph.Set.prod

modified def Homeomorph.Set.univ

modified def Homeomorph.Simps.symm_apply

modified theorem Homeomorph.apply_symm_apply

modified def Homeomorph.changeInv

modified theorem Homeomorph.coe_prodComm

modified theorem Homeomorph.coe_prodCongr

modified theorem Homeomorph.coe_punitProd

modified theorem Homeomorph.coe_symm_toEquiv

modified theorem Homeomorph.coe_toEquiv

modified theorem Homeomorph.coinduced_eq

modified theorem Homeomorph.comap_cocompact

modified theorem Homeomorph.comap_nhds_eq

modified theorem Homeomorph.comp_continuousAt_iff'

modified theorem Homeomorph.comp_continuousAt_iff

modified theorem Homeomorph.comp_continuousOn_iff

modified theorem Homeomorph.comp_continuousWithinAt_iff

modified theorem Homeomorph.comp_continuous_iff'

modified theorem Homeomorph.comp_continuous_iff

modified theorem Homeomorph.comp_isOpenMap_iff'

modified theorem Homeomorph.comp_isOpenMap_iff

modified theorem Homeomorph.ext

modified def Homeomorph.finTwoArrow

modified def Homeomorph.funSplitAt

modified def Homeomorph.funUnique

modified def Homeomorph.homeomorphOfContinuousOpen

modified def Homeomorph.homeomorphOfUnique

modified theorem Homeomorph.homeomorph_mk_coe

modified theorem Homeomorph.homeomorph_mk_coe_symm

modified def Homeomorph.image

modified theorem Homeomorph.image_closure

modified theorem Homeomorph.image_frontier

modified theorem Homeomorph.image_interior

modified theorem Homeomorph.image_preimage

modified theorem Homeomorph.image_symm

modified theorem Homeomorph.induced_eq

modified theorem Homeomorph.isClosed_image

modified theorem Homeomorph.isClosed_preimage

modified theorem Homeomorph.isCompact_image

modified theorem Homeomorph.isCompact_preimage

modified theorem Homeomorph.isConnected_image

modified theorem Homeomorph.isConnected_preimage

modified theorem Homeomorph.isOpen_image

modified theorem Homeomorph.isOpen_preimage

modified theorem Homeomorph.isPreconnected_image

modified theorem Homeomorph.isPreconnected_preimage

modified theorem Homeomorph.locallyConnectedSpace

modified theorem Homeomorph.map_cocompact

modified theorem Homeomorph.map_nhds_eq

modified theorem Homeomorph.nhds_eq_comap

modified def Homeomorph.piCongr

modified def Homeomorph.piCongrLeft

modified def Homeomorph.piCongrRight

modified theorem Homeomorph.piCongrRight_symm

modified def Homeomorph.piEquivPiSubtypeProd

modified def Homeomorph.piFinTwo.{u}

modified def Homeomorph.piSplitAt

modified theorem Homeomorph.preimage_closure

modified theorem Homeomorph.preimage_frontier

modified theorem Homeomorph.preimage_image

modified theorem Homeomorph.preimage_interior

modified theorem Homeomorph.preimage_symm

modified def Homeomorph.prodAssoc

modified def Homeomorph.prodComm

modified theorem Homeomorph.prodComm_symm

modified def Homeomorph.prodCongr

modified theorem Homeomorph.prodCongr_symm

modified def Homeomorph.prodPUnit

modified def Homeomorph.prodSumDistrib

modified def Homeomorph.punitProd

modified theorem Homeomorph.range_coe

modified theorem Homeomorph.refl_symm

modified theorem Homeomorph.self_comp_symm

modified theorem Homeomorph.self_trans_symm

modified def Homeomorph.setCongr

modified def Homeomorph.sigmaProdDistrib

modified def Homeomorph.sumCongr

modified def Homeomorph.sumProdDistrib

modified theorem Homeomorph.symm_apply_apply

modified theorem Homeomorph.symm_comp_self

modified theorem Homeomorph.symm_map_nhds_eq

modified theorem Homeomorph.symm_symm

modified theorem Homeomorph.symm_trans_apply

modified theorem Homeomorph.symm_trans_self

modified theorem Homeomorph.toEquiv_injective

modified theorem Homeomorph.trans_apply

modified def Homeomorph.ulift.{u,

modified structure Homeomorph