Mathlib.Topology.Defs.Sequences

Module docstring

{"# 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 "}

seqClosure definition

(s : Set X) : Set X

Full source

/-- 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 seqClosure (s : Set X) : Set X :=
  { a | ∃ x : ℕ → X, (∀ n : ℕ, x n ∈ s) ∧ Tendsto x atTop (𝓝 a) }

Sequential closure of a set

Informal description

The sequential closure of a set $s$ in a topological space $X$ is the set of all points $a \in X$ for which there exists a sequence $(x_n)_{n \in \mathbb{N}}$ in $s$ that converges to $a$.

IsSeqClosed definition

(s : Set X) : Prop

Full source

/-- 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 IsSeqClosed (s : Set X) : Prop :=
  ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, (∀ n, x n ∈ s) → Tendsto x atTop (𝓝 p) → p ∈ s

Sequentially closed set

Informal description

A set $s$ in a topological space $X$ is called *sequentially closed* if for every sequence $(x_n)_{n \in \mathbb{N}}$ in $s$ that converges to a point $p \in X$, the limit $p$ belongs to $s$.

SeqContinuous definition

(f : X → Y) : Prop

Full source

/-- A function between topological spaces is sequentially continuous if it commutes with limit of
 convergent sequences. -/
def SeqContinuous (f : X → Y) : Prop :=
  ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, Tendsto x atTop (𝓝 p) → Tendsto (f ∘ x) atTop (𝓝 (f p))

Sequential continuity of a function

Informal description

A function $f \colon X \to Y$ between topological spaces is called *sequentially continuous* if for every sequence $(x_n)_{n \in \mathbb{N}}$ in $X$ converging to a point $p \in X$, the sequence $(f(x_n))_{n \in \mathbb{N}}$ converges to $f(p)$ in $Y$.

IsSeqCompact definition

(s : Set X)

Full source

/-- A set `s` is sequentially compact if every sequence taking values in `s` has a
converging subsequence. -/
def IsSeqCompact (s : Set X) :=
  ∀ ⦃x : ℕ → X⦄, (∀ n, x n ∈ s) → ∃ a ∈ s, ∃ φ : ℕ → ℕ, StrictMono φ ∧ Tendsto (x ∘ φ) atTop (𝓝 a)

Sequentially compact set

Informal description

A set $s$ in a topological space $X$ is called *sequentially compact* if every sequence $(x_n)_{n \in \mathbb{N}}$ with $x_n \in s$ for all $n$ has a subsequence $(x_{\varphi(n)})_{n \in \mathbb{N}}$ that converges to some point $a \in s$, where $\varphi \colon \mathbb{N} \to \mathbb{N}$ is strictly increasing.

SeqCompactSpace structure

Full source

/-- A space `X` is sequentially compact if every sequence in `X` has a
converging subsequence. -/
@[mk_iff]
class SeqCompactSpace : Prop where
  isSeqCompact_univ : IsSeqCompact (univ : Set X)

Sequentially compact space

Informal description

A topological space $ X $ is called *sequentially compact* if every sequence in $ X $ has a convergent subsequence.

FrechetUrysohnSpace structure

Full source

/-- 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. -/
class FrechetUrysohnSpace : Prop where
  closure_subset_seqClosure : ∀ s : Set X, closureclosure s ⊆ seqClosure s

Fréchet-Urysohn space

Informal description

A topological space $ X $ is called a *Fréchet-Urysohn space* if for every subset $ s \subseteq X $, the sequential closure of $ s $ (the set of all limits of sequences in $ s $) coincides with the topological closure of $ s $. Since the inclusion $ \text{seqClosure}(s) \subseteq \overline{s} $ always holds, the defining condition is the reverse inclusion $ \overline{s} \subseteq \text{seqClosure}(s) $.

SequentialSpace structure

Full source

/-- 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. -/
class SequentialSpace : Prop where
  isClosed_of_seq : ∀ s : Set X, IsSeqClosed s → IsClosed s

Sequential Space

Informal description

A topological space $ X $ is called a *sequential space* if every sequentially closed subset of $ X $ is closed. Here, a subset $ s \subseteq X $ is sequentially closed if it contains all limit points of sequences in $ s $.

IsSeqClosed.isClosed theorem

[SequentialSpace X] {s : Set X} (hs : IsSeqClosed s) : IsClosed s

Full source

/-- In a sequential space, a sequentially closed set is closed. -/
protected theorem IsSeqClosed.isClosed [SequentialSpace X] {s : Set X} (hs : IsSeqClosed s) :
    IsClosed s :=
  SequentialSpace.isClosed_of_seq s hs

Sequentially closed sets are closed in a sequential space

Informal description

In a sequential space $X$, if a subset $s \subseteq X$ is sequentially closed, then $s$ is closed.