Commit 2021-10-23 17:11 36f8c1db

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