[Merged by Bors] - refactor(order/filter/bases): turn is_countably_generated into a class

[urkud]

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).

---

@PatrickMassot Do you want me to restore some of the deleted definitions/lemmas? Should I move lemmas that now automatically work for metric spaces (uniform_space.second_countable_of_separable etc) to the root namespace?

[PatrickMassot]

What's the motivation for removing lemmas?

[urkud]

Do you mean lemmas in the is_countably_generated namespace? None of them were used in mathlib and I think that filter.exists_antitone_basis and filter.has_basis.exists_antitone_subbasis should be the main APIs for countably generated filters. I can restore them back in the filter.is_countably_generated NS if you want; can't move them to the filter NS because of name clashes.
As for lemmas in the (e)metric namespace, earlier they provided the is_countably_generated argument to their uniform_space counterparts but now typeclass instances can do it.

[PatrickMassot]

bors merge

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests