mathlib3

36f8c1db - refactor(order/filter/bases): turn `is_countably_generated` into a class (#9838)

refactor(order/filter/bases): turn `is_countably_generated` into a class (#9838) ## API changes ### Filters * turn `filter.is_countably_generated` into a class, turn some lemmas into instances; * remove definition/lemmas (all were in the `filter.is_countably_generated` namespace): `generating_set`, `countable_generating_set`, `eq_generate`, `countable_filter_basis`, `filter_basis_filter`, `has_countable_basis`, `exists_countable_infi_principal`, `exists_seq`; * rename `filter.is_countably_generated.exists_antitone_subbasis` to `filter.has_basis.exists_antitone_subbasis`; * rename `filter.is_countably_generated.exists_antitone_basis` to `filter.exists_antitone_basis`; * rename `filter.is_countably_generated.exists_antitone_seq'` to `filter.exists_antitone_seq`; * rename `filter.is_countably_generated.exists_seq` to `filter.exists_antitone_eq_infi_principal`; * rename `filter.is_countably_generated.tendsto_iff_seq_tendsto` to `filter.tendsto_iff_seq_tendsto`; * rename `filter.is_countably_generated.tendsto_of_seq_tendsto` to `filter.tendsto_of_seq_tendsto`; * slightly generalize `is_countably_generated_at_top` and `is_countably_generated_at_bot`; * add `filter.generate_eq_binfi`; ### Topology * merge `is_closed.is_Gδ` with `is_closed.is_Gδ'`; * merge `is_Gδ_set_of_continuous_at_of_countably_generated_uniformity` with `is_Gδ_set_of_continuous_at`; * merge `is_lub.exists_seq_strict_mono_tendsto_of_not_mem'` with `is_lub.exists_seq_strict_mono_tendsto_of_not_mem`; * merge `is_lub.exists_seq_monotone_tendsto'` with `is_lub.exists_seq_monotone_tendsto`; * merge `is_glb.exists_seq_strict_anti_tendsto_of_not_mem'` with `is_glb.exists_seq_strict_anti_tendsto_of_not_mem`; * merge `is_glb.exists_seq_antitone_tendsto'` with `is_glb.exists_seq_antitone_tendsto`; * drop `emetric.first_countable_topology`, turn `uniform_space.first_countable_topology` into an instance; * drop `emetric.second_countable_of_separable`, use `uniform_space.second_countable_of_separable` instead; * drop `metric.compact_iff_seq_compact`, use `uniform_space.compact_iff_seq_compact` instead; * drop `metric.compact_space_iff_seq_compact_space`, use `uniform_space.compact_space_iff_seq_compact_space` instead; ## Measure theory and integrals Various lemmas assume `[is_countably_generated l]` instead of `(h : is_countably_generated l)`.