filter.has_countable_basis

A filter has a countable basis iff it is generated by a countable collection of subsets of α. (A filter is a generated by a collection of sets iff it is the infimum of the principal filters.)

Note: we do not require the collection to be closed under finite intersections.

filter.has_countable_basis_iff_seq

Different characterization of countable basis. A filter has a countable basis iff it is generated by a sequence of sets.

filter.has_countable_basis_iff_mono_seq

Different characterization of countable basis. A filter has a countable basis iff it is generated by a monotonically decreasing sequence of sets.

topological_space.is_topological_basis

A topological basis is one that satisfies the necessary conditions so that it suffices to take unions of the basis sets to get a topology (without taking finite intersections as well).

topological_space.separable_space

A separable space is one with a countable dense subset.

topological_space.first_countable_topology

A first-countable space is one in which every point has a countable neighborhood basis.

topological_space.second_countable_topology

A second-countable space is one with a countable basis.