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

def seqClosure {X : Type u_1} [TopologicalSpace X] (s : Set X) : Set X

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.

def IsSeqClosed {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

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.

def SeqContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop

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

def IsSeqCompact {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

A set s is sequentially compact if every sequence taking values in s has a converging subsequence.

class SeqCompactSpace (X : Type u_1) [TopologicalSpace X] : Prop

A space X is sequentially compact if every sequence in X has a converging subsequence.

• isSeqCompact_univ : IsSeqCompact Set.univ

theorem seqCompactSpace_iff (X : Type u_1) [TopologicalSpace X] : SeqCompactSpace X ↔ IsSeqCompact Set.univ

class FrechetUrysohnSpace (X : Type u_1) [TopologicalSpace X] : Prop

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

class SequentialSpace (X : Type u_1) [TopologicalSpace X] : Prop

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

theorem IsSeqClosed.isClosed {X : Type u_1} [TopologicalSpace X] [SequentialSpace X] {s : Set X} (hs : IsSeqClosed s) : IsClosed s

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