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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

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.isSeqCompact_univ {X : Type u_1} [TopologicalSpace X] [self : SeqCompactSpace X] : IsSeqCompact Set.univ

@[deprecated SeqCompactSpace.isSeqCompact_univ]

theorem seq_compact_univ {X : Type u_1} [TopologicalSpace X] [self : SeqCompactSpace X] : IsSeqCompact Set.univ

Alias of SeqCompactSpace.isSeqCompact_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

theorem FrechetUrysohnSpace.closure_subset_seqClosure {X : Type u_1} [TopologicalSpace X] [self : FrechetUrysohnSpace X] (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 SequentialSpace.isClosed_of_seq {X : Type u_1} [TopologicalSpace X] [self : SequentialSpace X] (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.