mathlib

eff9ed3a - feat(topology/uniform_space): some basic lemmas (#3123)

feat(topology/uniform_space): some basic lemmas (#3123) This is the second PR on the road to Heine. It contains various elementary lemmas about uniform spaces.