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