mathlib

26f41120 - feat(topology/uniform_space/separation): add `filter.has_basis.mem_separation_rel` (#14050)

feat(topology/uniform_space/separation): add `filter.has_basis.mem_separation_rel` (#14050) * add `filter.has_basis.mem_separation_rel`; * add `filter.has_basis.forall_mem_mem`, use it in `filter.has_basis.sInter_sets`; * replace two remaining `lift' powerset` with `small_sets`.