# Sequences in topological spaces #

In this file we prove theorems about relations between closure/compactness/continuity etc and their sequential counterparts.

## Main definitions #

The following notions are defined in `Topology/Defs/Sequences`

.
We build theory about these definitions here, so we remind the 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;`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 is contained in the closure of that set. The converse is not true.

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.

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.

## Equations

- ⋯ = ⋯

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

## Equations

- ⋯ = ⋯

**Alias** of `IsInducing.frechetUrysohnSpace`

.

Subtype of a Fréchet-Urysohn space is a Fréchet-Urysohn space.

## Equations

- ⋯ = ⋯

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

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.

**Alias** of `IsQuotientMap.sequentialSpace`

.

The quotient of a sequential space is a sequential space.

## Equations

- ⋯ = ⋯

The sum (disjoint union) of two sequential spaces is a sequential space.

## Equations

- ⋯ = ⋯

The disjoint union of an indexed family of sequential spaces is a sequential space.

## Equations

- ⋯ = ⋯

## Equations

- ⋯ = ⋯

Sequential compactness of sets is preserved under sequentially continuous functions.

The range of sequentially continuous function on a sequentially compact space is sequentially compact.

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