# Commit 2021-10-23 17:11 36f8c1db

View on Github →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)`

.