mathlib

c8738cb6 - feat(topology/uniform_space/cauchy): generalize `second_countable_of_separable` to uniform spaces (#4530)

feat(topology/uniform_space/cauchy): generalize `second_countable_of_separable` to uniform spaces (#4530) Also generalize `is_countably_generated.has_antimono_basis` to `is_countably_generated.exists_antimono_subbasis` and add a few lemmas about bases of the uniformity filter.