mathlib

a4efbb0e - feat(topology/uniform_space): local uniform convergence on union (#16883)

feat(topology/uniform_space): local uniform convergence on union (#16883) I'm pretty confident these need some assumption like open-ness, but maybe something weaker is enough? Co-authored-by: Bhavik Mehta <bm489@cam.ac.uk>