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} [] (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.

Equations
Instances For
def IsSeqClosed {X : Type u_1} [] (s : Set X) :

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
Instances For
def SeqContinuous {X : Type u_1} {Y : Type u_2} [] [] (f : XY) :

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

Equations
Instances For
def IsSeqCompact {X : Type u_1} [] (s : Set X) :

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

Equations
Instances For
theorem seqCompactSpace_iff (X : Type u_1) [] :
IsSeqCompact Set.univ
class SeqCompactSpace (X : Type u_1) [] :

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

Instances
theorem SeqCompactSpace.seq_compact_univ {X : Type u_1} [] [self : ] :
IsSeqCompact Set.univ
class FrechetUrysohnSpace (X : Type u_1) [] :

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),
Instances
theorem FrechetUrysohnSpace.closure_subset_seqClosure {X : Type u_1} [] [self : ] (s : Set X) :
class SequentialSpace (X : Type u_1) [] :

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),
Instances
theorem SequentialSpace.isClosed_of_seq {X : Type u_1} [] [self : ] (s : Set X) :
theorem IsSeqClosed.isClosed {X : Type u_1} [] [] {s : Set X} (hs : ) :

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