Commit 2023-02-11 08:36 efa2c475

View on Github →

feat: port Topology.UniformSpace.Equiv (#2092)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/Equiv.lean

added def Equiv.toUniformEquivOfUniformInducing

added def UniformEquiv.Simps.apply

added def UniformEquiv.Simps.symm_apply

added theorem UniformEquiv.apply_symm_apply

added def UniformEquiv.changeInv

added theorem UniformEquiv.coe_prodComm

added theorem UniformEquiv.coe_prodCongr

added theorem UniformEquiv.coe_punitProd

added theorem UniformEquiv.coe_symm_toEquiv

added theorem UniformEquiv.coe_toEquiv

added theorem UniformEquiv.comap_eq

added theorem UniformEquiv.ext

added def UniformEquiv.finTwoArrow

added def UniformEquiv.funUnique

added def UniformEquiv.image

added theorem UniformEquiv.image_preimage

added theorem UniformEquiv.image_symm

added def UniformEquiv.piFinTwo

added theorem UniformEquiv.preimage_image

added theorem UniformEquiv.preimage_symm

added def UniformEquiv.prodAssoc

added def UniformEquiv.prodComm

added theorem UniformEquiv.prodComm_symm

added def UniformEquiv.prodCongr

added theorem UniformEquiv.prodCongr_symm

added def UniformEquiv.prodPunit

added def UniformEquiv.punitProd

added theorem UniformEquiv.range_coe

added theorem UniformEquiv.refl_symm

added theorem UniformEquiv.self_comp_symm

added def UniformEquiv.setCongr

added theorem UniformEquiv.symm_apply_apply

added theorem UniformEquiv.symm_comp_self

added theorem UniformEquiv.toEquiv_injective

added theorem UniformEquiv.toHomeomorph_apply

added theorem UniformEquiv.toHomeomorph_symm_apply

added theorem UniformEquiv.trans_apply

added def UniformEquiv.ulift

added theorem UniformEquiv.uniformEquiv_mk_coe

added theorem UniformEquiv.uniformEquiv_mk_coe_symm

added structure UniformEquiv