mathlib

04ed867a - chore(topology/uniform_space/cauchy): add a few simple lemmas (#9685)

chore(topology/uniform_space/cauchy): add a few simple lemmas (#9685) * rename `cauchy_prod` to `cauchy.prod`; * add `cauchy_seq.tendsto_uniformity`, `cauchy_seq.nonempty`, `cauchy_seq.comp_tendsto`, `cauchy_seq.prod`, `cauchy_seq.prod_map`, `uniform_continuous.comp_cauchy_seq`, and `filter.tendsto.subseq_mem_entourage`; * drop `[nonempty _]` assumption in `cauchy_seq.mem_entourage`.