mathlib

26918a05 - feat(topology/metric_space/baire): define filter `residual` (#3149)

feat(topology/metric_space/baire): define filter `residual` (#3149) Fixes #2265. Also define a typeclass `countable_Inter_filter` and prove that both `residual` and `μ.ae` have this property.