# Sequences in topological spaces #

In this file we define sequential closure, continuity, compactness etc.

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

## Tags #

sequentially closed, sequentially compact, sequential space

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.

## Equations

- seqClosure s = {a : X | ∃ (x : ℕ → X), (∀ (n : ℕ), x n ∈ s) ∧ Filter.Tendsto x Filter.atTop (nhds a)}

## Instances For

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.

## Equations

- IsSeqClosed s = ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, (∀ (n : ℕ), x n ∈ s) → Filter.Tendsto x Filter.atTop (nhds p) → p ∈ s

## Instances For

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

## Equations

- SeqContinuous f = ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, Filter.Tendsto x Filter.atTop (nhds p) → Filter.Tendsto (f ∘ x) Filter.atTop (nhds (f p))

## Instances For

A set `s`

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

has a
converging subsequence.

## Equations

- IsSeqCompact s = ∀ ⦃x : ℕ → X⦄, (∀ (n : ℕ), x n ∈ s) → ∃ a ∈ s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

## Instances For

A space `X`

is sequentially compact if every sequence in `X`

has a
converging subsequence.

- seq_compact_univ : IsSeqCompact Set.univ

## Instances

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.

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

## Instances

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.

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

## Instances

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