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

theorem subset_seqClosure {X : Type u_1} [] {s : Set X} :
s
theorem seqClosure_subset_closure {X : Type u_1} [] {s : Set X} :

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

theorem IsSeqClosed.seqClosure_eq {X : Type u_1} [] {s : Set X} (hs : ) :
= s

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

theorem isSeqClosed_of_seqClosure_eq {X : Type u_1} [] {s : Set X} (hs : = s) :

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

theorem isSeqClosed_iff {X : Type u_1} [] {s : Set X} :
= s

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

theorem IsClosed.isSeqClosed {X : Type u_1} [] {s : Set X} (hc : ) :

A set is sequentially closed if it is closed.

theorem seqClosure_eq_closure {X : Type u_1} [] (s : Set X) :
theorem mem_closure_iff_seq_limit {X : Type u_1} [] {s : Set X} {a : X} :
a ∃ (x : X), (∀ (n : ), x n s) Filter.Tendsto x Filter.atTop (nhds a)

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.

theorem tendsto_nhds_iff_seq_tendsto {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {a : X} {b : Y} :
Filter.Tendsto f (nhds a) (nhds b) ∀ (u : X), Filter.Tendsto u Filter.atTop (nhds a)Filter.Tendsto (f u) Filter.atTop (nhds b)

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.

theorem FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto {X : Type u_1} [] (h : ∀ (f : XProp) (a : X), (∀ (u : X), Filter.Tendsto u Filter.atTop (nhds a)Filter.Tendsto (f u) Filter.atTop (nhds (f a)))) :

An alternative construction for FrechetUrysohnSpace: if sequential convergence implies convergence, then the space is a Fréchet-Urysohn space.

@[instance 100]

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

Equations
• =
@[instance 100]

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

Equations
• =
theorem Inducing.frechetUrysohnSpace {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
instance Subtype.instFrechetUrysohnSpace {X : Type u_1} [] {p : XProp} :

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

Equations
• =
theorem isSeqClosed_iff_isClosed {X : Type u_1} [] [] {M : Set X} :

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

theorem IsSeqClosed.preimage {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set Y} (hs : ) (hf : ) :

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

theorem Continuous.seqContinuous {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) :
theorem SeqContinuous.continuous {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) :

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

theorem continuous_iff_seqContinuous {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} :

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

theorem SequentialSpace.coinduced {X : Type u_1} {Y : Type u_2} [] [] (f : XY) :
theorem SequentialSpace.iSup {X : Type u_1} {ι : Sort u_3} {t : ι} (h : ∀ (i : ι), ) :
theorem SequentialSpace.sup {X : Type u_1} {t₁ : } {t₂ : } (h₁ : ) (h₂ : ) :
theorem QuotientMap.sequentialSpace {X : Type u_1} {Y : Type u_2} [] [] [] {f : XY} (hf : ) :
instance Quotient.instSequentialSpace {X : Type u_1} [] [] {s : } :

The quotient of a sequential space is a sequential space.

Equations
• =
instance Sum.instSequentialSpace {X : Type u_1} {Y : Type u_2} [] [] [] [] :

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

Equations
• =
instance Sigma.instSequentialSpace {ι : Type u_3} {X : ιType u_4} [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), SequentialSpace (X i)] :
SequentialSpace ((i : ι) × X i)

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

Equations
• =
theorem IsSeqCompact.subseq_of_frequently_in {X : Type u_1} [] {s : Set X} (hs : ) {x : X} (hx : ∃ᶠ (n : ) in Filter.atTop, x n s) :
as, ∃ (φ : ), Filter.Tendsto (x φ) Filter.atTop (nhds a)
theorem SeqCompactSpace.tendsto_subseq {X : Type u_1} [] [] (x : X) :
∃ (a : X) (φ : ), Filter.Tendsto (x φ) Filter.atTop (nhds a)
theorem IsCompact.isSeqCompact {X : Type u_1} [] {s : Set X} (hs : ) :
theorem IsCompact.tendsto_subseq' {X : Type u_1} [] {s : Set X} {x : X} (hs : ) (hx : ∃ᶠ (n : ) in Filter.atTop, x n s) :
as, ∃ (φ : ), Filter.Tendsto (x φ) Filter.atTop (nhds a)
theorem IsCompact.tendsto_subseq {X : Type u_1} [] {s : Set X} {x : X} (hs : ) (hx : ∀ (n : ), x n s) :
as, ∃ (φ : ), Filter.Tendsto (x φ) Filter.atTop (nhds a)
@[instance 100]
Equations
• =
theorem CompactSpace.tendsto_subseq {X : Type u_1} [] [] (x : X) :
∃ (a : X) (φ : ), Filter.Tendsto (x φ) Filter.atTop (nhds a)
theorem IsSeqCompact.exists_tendsto_of_frequently_mem {X : Type u_1} [] {s : Set X} (hs : ) {u : X} (hu : ∃ᶠ (n : ) in Filter.atTop, u n s) (huc : ) :
xs, Filter.Tendsto u Filter.atTop (nhds x)
theorem IsSeqCompact.exists_tendsto {X : Type u_1} [] {s : Set X} (hs : ) {u : X} (hu : ∀ (n : ), u n s) (huc : ) :
xs, Filter.Tendsto u Filter.atTop (nhds x)
theorem IsSeqCompact.totallyBounded {X : Type u_1} [] {s : Set X} (h : ) :

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

theorem IsSeqCompact.isComplete {X : Type u_1} [] {s : Set X} [().IsCountablyGenerated] (hs : ) :

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

theorem IsSeqCompact.isCompact {X : Type u_1} [] {s : Set X} [().IsCountablyGenerated] (hs : ) :

If 𝓤 β is countably generated, then any sequentially compact set is compact.

theorem UniformSpace.isCompact_iff_isSeqCompact {X : Type u_1} [] {s : Set X} [().IsCountablyGenerated] :

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.

theorem UniformSpace.compactSpace_iff_seqCompactSpace {X : Type u_1} [] [().IsCountablyGenerated] :