mathlib

79df8cc4 - refactor(order/filter/at_top): import order.filter.bases (#3523)

refactor(order/filter/at_top): import order.filter.bases (#3523) This way we can use facts about `filter.has_basis` in `filter.at_top`. Also generalize `is_countably_generated_at_top_finset_nat` to `at_top` filter on any `encodable` type.