Sequences in topological spaces #
In this file we define sequences in topological spaces and show how they are related to filters and the topology. In particular, we
- define the sequential closure of a set and prove that it's contained in the closure,
- define a type class "sequential_space" in which closure and sequential closure agree,
- define sequential continuity and show that it coincides with continuity in sequential spaces,
- provide an instance that shows that every first-countable (and in particular metric) space is a sequential space.
- define sequential compactness, prove that compactness implies sequential compactness in first countable spaces, and prove they are equivalent for uniform spaces having a countable uniformity basis (in particular metric spaces).
Sequential closures, sequential continuity, and sequential spaces. #
A sequence converges in the sence of topological spaces iff the associated statement for filter holds.
The sequential closure of a subset M ⊆ α of a topological space α is the set of all p ∈ α which arise as limit of sequences in M.
A sequential space is a space in which 'sequences are enough to probe the topology'. This can be formalised by demanding that the sequential closure and the closure coincide. The following statements show that other topological properties can be deduced from sequences in sequential spaces.
In a sequential space, a point belongs to the closure of a set iff it is a limit of a sequence taking values in this set.
A function between topological spaces is sequentially continuous if it commutes with limit of convergent sequences.
Every first-countable space is sequential.
s is sequentially compact if every sequence taking values in
s has a
A version of Bolzano-Weistrass: in a uniform space with countably generated uniformity filter (e.g., in a metric space), a set is compact if and only if it is sequentially compact.
A version of Bolzano-Weistrass: in a proper metric space (eg. $ℝ^n$), every bounded sequence has a converging subsequence. This version assumes only that the sequence is frequently in some bounded set.
A version of Bolzano-Weistrass: in a proper metric space (eg. $ℝ^n$), every bounded sequence has a converging subsequence.