Commit 2022-06-10 14:50 18936e55

View on Github →

feat(topology/uniform_space/equiv): define uniform isomorphisms (#14537) This adds a new file, mostly copy-pasted from topology/homeomorph, to analogously define uniform isomorphisms

Estimated changes

Modified src/data/prod/basic.lean

modified theorem prod.id_prod

added theorem prod.map_id

Modified src/topology/uniform_space/basic.lean

added theorem uniform_continuous_subtype_coe

Created src/topology/uniform_space/equiv.lean

added def equiv.to_uniform_equiv_of_uniform_inducing

added theorem uniform_equiv.apply_symm_apply

added def uniform_equiv.change_inv

added theorem uniform_equiv.coe_prod_comm

added theorem uniform_equiv.coe_prod_congr

added theorem uniform_equiv.coe_punit_prod

added theorem uniform_equiv.coe_symm_to_equiv

added theorem uniform_equiv.coe_to_equiv

added theorem uniform_equiv.comap_eq

added theorem uniform_equiv.ext

added def uniform_equiv.fin_two_arrow

added def uniform_equiv.fun_unique

added def uniform_equiv.image

added theorem uniform_equiv.image_preimage

added theorem uniform_equiv.image_symm

added theorem uniform_equiv.preimage_image

added theorem uniform_equiv.preimage_symm

added def uniform_equiv.prod_assoc

added def uniform_equiv.prod_comm

added theorem uniform_equiv.prod_comm_symm

added def uniform_equiv.prod_congr

added theorem uniform_equiv.prod_congr_symm

added def uniform_equiv.prod_punit

added def uniform_equiv.punit_prod

added theorem uniform_equiv.range_coe

added theorem uniform_equiv.refl_symm

added theorem uniform_equiv.self_comp_symm

added def uniform_equiv.set_congr

added def uniform_equiv.simps.apply

added def uniform_equiv.simps.symm_apply

added theorem uniform_equiv.symm_apply_apply

added theorem uniform_equiv.symm_comp_self

added theorem uniform_equiv.to_equiv_injective

added theorem uniform_equiv.trans_apply

added theorem uniform_equiv.uniform_equiv_mk_coe

added theorem uniform_equiv.uniform_equiv_mk_coe_symm

added def uniform_equiv.{u}

added structure uniform_equiv

Modified src/topology/uniform_space/uniform_embedding.lean

added theorem uniform_inducing_id

added theorem uniform_inducing_of_compose