# Sequences in topological spaces #

In this file we define sequences in topological spaces and show how they are related to filters and the topology.

## Main definitions #

### Set operation #

`seqClosure s`

: sequential closure of a set, the set of limits of sequences of points of`s`

;

### Predicates #

`IsSeqClosed s`

: predicate saying that a set is sequentially closed, i.e.,`seqClosure s ⊆ s`

;`SeqContinuous f`

: predicate saying that a function is sequentially continuous, i.e., for any sequence`u : ℕ → X`

that converges to a point`x`

, the sequence`f ∘ u`

converges to`f x`

;`IsSeqCompact s`

: predicate saying that a set is sequentially compact, i.e., every sequence taking values in`s`

has a converging subsequence.

### Type classes #

`FrechetUrysohnSpace X`

: a typeclass saying that a topological space is a*Fréchet-Urysohn space*, i.e., the sequential closure of any set is equal to its closure.`SequentialSpace X`

: a typeclass saying that a topological space is a*sequential space*, i.e., any sequentially closed set in this space is closed. This condition is weaker than being a Fréchet-Urysohn space.`SeqCompactSpace X`

: a typeclass saying that a topological space is sequentially compact, i.e., every sequence in`X`

has a converging subsequence.

## Main results #

`seqClosure_subset_closure`

: closure of a set includes its sequential closure;`IsClosed.isSeqClosed`

: a closed set is sequentially closed;`IsSeqClosed.seqClosure_eq`

: sequential closure of a sequentially closed set`s`

is equal to`s`

;`seqClosure_eq_closure`

: in a Fréchet-Urysohn space, the sequential closure of a set is equal to its closure;`tendsto_nhds_iff_seq_tendsto`

,`FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto`

: a topological space is a Fréchet-Urysohn space if and only if sequential convergence implies convergence;`TopologicalSpace.FirstCountableTopology.frechetUrysohnSpace`

: every topological space with first countable topology is a Fréchet-Urysohn space;`FrechetUrysohnSpace.to_sequentialSpace`

: every Fréchet-Urysohn space is a sequential space;`IsSeqCompact.isCompact`

: a sequentially compact set in a uniform space with countably generated uniformity is compact.

## Tags #

sequentially closed, sequentially compact, sequential space

### Sequential closures, sequential continuity, and sequential spaces. #

The sequential closure of a set `s : Set X`

in a topological space `X`

is the set of all `a : X`

which arise as limit of sequences in `s`

. Note that the sequential closure of a set is not
guaranteed to be sequentially closed.

## Instances For

The sequential closure of a set is contained in the closure of that set. The converse is not true.

A set `s`

is sequentially closed if for any converging sequence `x n`

of elements of `s`

, the
limit belongs to `s`

as well. Note that the sequential closure of a set is not guaranteed to be
sequentially closed.

## Instances For

The sequential closure of a sequentially closed set is the set itself.

If a set is equal to its sequential closure, then it is sequentially closed.

A set is sequentially closed iff it is equal to its sequential closure.

A set is sequentially closed if it is closed.

- closure_subset_seqClosure : ∀ (s : Set X), closure s ⊆ seqClosure s

A topological space is called a *Fréchet-Urysohn space*, if the sequential closure of any set
is equal to its closure. Since one of the inclusions is trivial, we require only the non-trivial one
in the definition.

## Instances

In a Fréchet-Urysohn space, a point belongs to the closure of a set iff it is a limit of a sequence taking values in this set.

If the domain of a function `f : α → β`

is a Fréchet-Urysohn space, then convergence
is equivalent to sequential convergence. See also `Filter.tendsto_iff_seq_tendsto`

for a version
that works for any pair of filters assuming that the filter in the domain is countably generated.

This property is equivalent to the definition of `FrechetUrysohnSpace`

, see
`FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto`

.

An alternative construction for `FrechetUrysohnSpace`

: if sequential convergence implies
convergence, then the space is a Fréchet-Urysohn space.

Every first-countable space is a Fréchet-Urysohn space.

- isClosed_of_seq : ∀ (s : Set X), IsSeqClosed s → IsClosed s

A topological space is said to be a *sequential space* if any sequentially closed set in this
space is closed. This condition is weaker than being a Fréchet-Urysohn space.

## Instances

Every Fréchet-Urysohn space is a sequential space.

In a sequential space, a sequentially closed set is closed.

In a sequential space, a set is closed iff it's sequentially closed.

A function between topological spaces is sequentially continuous if it commutes with limit of convergent sequences.

## Instances For

The preimage of a sequentially closed set under a sequentially continuous map is sequentially closed.

A sequentially continuous function defined on a sequential space is continuous.

If the domain of a function is a sequential space, then continuity of this function is equivalent to its sequential continuity.

The quotient of a sequential space is a sequential space.

A set `s`

is sequentially compact if every sequence taking values in `s`

has a
converging subsequence.

## Instances For

- seq_compact_univ : IsSeqCompact Set.univ

A space `X`

is sequentially compact if every sequence in `X`

has a
converging subsequence.

## Instances

A sequentially compact set in a uniform space is totally bounded.

A sequentially compact set in a uniform set with countably generated uniformity filter is complete.

If `𝓤 β`

is countably generated, then any sequentially compact set is compact.

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.