mathlib3

aed7f9af - feat(topology/uniform_space/basic): add three easy lemmas about `uniform_space.comap` (#14678)

feat(topology/uniform_space/basic): add three easy lemmas about `uniform_space.comap` (#14678) These are uniform spaces versions of `filter.comap_inf`, `filter.comap_infi` and `filter.comap_mono`. I split them from #14534 which is already a quite big PR.