mathlib documentation

topology.sequences

Sequences in topological spaces #

In this file we define sequences in topological spaces and show how they are related to filters and the topology.

Main definitions #

Set operation #

Predicates #

Type classes #

Main results #

Tags #

sequentially closed, sequentially compact, sequential space

Sequential closures, sequential continuity, and sequential spaces. #

def seq_closure {X : Type u_1} [topological_space 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
theorem subset_seq_closure {X : Type u_1} [topological_space X] {s : set X} :

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

def is_seq_closed {X : Type u_1} [topological_space 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
theorem is_seq_closed.seq_closure_eq {X : Type u_1} [topological_space X] {s : set X} (hs : is_seq_closed s) :

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

theorem is_seq_closed_of_seq_closure_eq {X : Type u_1} [topological_space X] {s : set X} (hs : seq_closure s = s) :

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

theorem is_seq_closed_iff {X : Type u_1} [topological_space X] {s : set X} :

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

@[protected]
theorem is_closed.is_seq_closed {X : Type u_1} [topological_space X] {s : set X} (hc : is_closed s) :

A set is sequentially closed if it is closed.

@[class]
structure frechet_urysohn_space (X : Type u_3) [topological_space 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.

Instances of this typeclass
theorem mem_closure_iff_seq_limit {X : Type u_1} [topological_space X] [frechet_urysohn_space X] {s : set X} {a : X} :
a closure s (x : X), ( (n : ), x n s) filter.tendsto x filter.at_top (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.

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 frechet_urysohn_space, see frechet_urysohn_space.of_seq_tendsto_imp_tendsto.

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

@[protected, instance]

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

@[class]
structure sequential_space (X : Type u_3) [topological_space 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.

Instances of this typeclass
@[protected, instance]

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

@[protected]

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

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

def seq_continuous {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] (f : X Y) :
Prop

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

Equations
theorem is_seq_closed.preimage {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X Y} {s : set Y} (hs : is_seq_closed s) (hf : seq_continuous f) :

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

@[protected]
theorem continuous.seq_continuous {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] {f : X Y} (hf : continuous f) :
@[protected]
theorem seq_continuous.continuous {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] [sequential_space X] {f : X Y} (hf : seq_continuous f) :

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

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

@[protected, instance]

The quotient of a sequential space is a sequential space.

def is_seq_compact {X : Type u_1} [topological_space X] (s : set X) :
Prop

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

Equations
@[class]
structure seq_compact_space (X : Type u_3) [topological_space X] :
Prop

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

Instances of this typeclass
theorem is_seq_compact.subseq_of_frequently_in {X : Type u_1} [topological_space X] {s : set X} (hs : is_seq_compact s) {x : X} (hx : ∃ᶠ (n : ) in filter.at_top, x n s) :
(a : X) (H : a s) (φ : ), strict_mono φ filter.tendsto (x φ) filter.at_top (nhds a)
theorem is_compact.tendsto_subseq' {X : Type u_1} [topological_space X] [topological_space.first_countable_topology X] {s : set X} {x : X} (hs : is_compact s) (hx : ∃ᶠ (n : ) in filter.at_top, x n s) :
(a : X) (H : a s) (φ : ), strict_mono φ filter.tendsto (x φ) filter.at_top (nhds a)
theorem is_compact.tendsto_subseq {X : Type u_1} [topological_space X] [topological_space.first_countable_topology X] {s : set X} {x : X} (hs : is_compact s) (hx : (n : ), x n s) :
(a : X) (H : a s) (φ : ), strict_mono φ filter.tendsto (x φ) filter.at_top (nhds a)
theorem is_seq_compact.exists_tendsto_of_frequently_mem {X : Type u_1} [uniform_space X] {s : set X} (hs : is_seq_compact s) {u : X} (hu : ∃ᶠ (n : ) in filter.at_top, u n s) (huc : cauchy_seq u) :
(x : X) (H : x s), filter.tendsto u filter.at_top (nhds x)
theorem is_seq_compact.exists_tendsto {X : Type u_1} [uniform_space X] {s : set X} (hs : is_seq_compact s) {u : X} (hu : (n : ), u n s) (huc : cauchy_seq u) :
(x : X) (H : x s), filter.tendsto u filter.at_top (nhds x)
@[protected]

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

@[protected]

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

@[protected]

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

@[protected]

A version of Bolzano-Weistrass: 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 seq_compact.lebesgue_number_lemma_of_metric {X : Type u_1} [pseudo_metric_space X] {ι : Sort u_2} {c : ι set X} {s : set X} (hs : is_seq_compact s) (hc₁ : (i : ι), is_open (c i)) (hc₂ : s (i : ι), c i) :
(δ : ) (H : δ > 0), (a : X), a s ( (i : ι), metric.ball a δ c i)
theorem tendsto_subseq_of_frequently_bounded {X : Type u_1} [pseudo_metric_space X] [proper_space X] {s : set X} (hs : metric.bounded s) {x : X} (hx : ∃ᶠ (n : ) in filter.at_top, x n s) :
(a : X) (H : a closure s) (φ : ), strict_mono φ filter.tendsto (x φ) filter.at_top (nhds a)

A version of Bolzano-Weistrass: in a proper metric space (eg. $ℝ^n$), every bounded sequence has a converging subsequence. This version assumes only that the sequence is frequently in some bounded set.

theorem tendsto_subseq_of_bounded {X : Type u_1} [pseudo_metric_space X] [proper_space X] {s : set X} (hs : metric.bounded s) {x : X} (hx : (n : ), x n s) :
(a : X) (H : a closure s) (φ : ), strict_mono φ filter.tendsto (x φ) filter.at_top (nhds a)

A version of Bolzano-Weistrass: in a proper metric space (eg. $ℝ^n$), every bounded sequence has a converging subsequence.