Sequences in topological spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

Set operation #

seq_closure s: sequential closure of a set, the set of limits of sequences of points of s;

Predicates #

is_seq_closed s: predicate saying that a set is sequentially closed, i.e., seq_closure s ⊆ s;
seq_continuous 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;
is_seq_compact s: predicate saying that a set is sequentially compact, i.e., every sequence taking values in s has a converging subsequence.

Type classes #

frechet_urysohn_space 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.
sequential_space 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.
seq_compact_space X: a typeclass saying that a topological space is sequentially compact, i.e., every sequence in X has a converging subsequence.

Main results #

seq_closure_subset_closure: closure of a set includes its sequential closure;
is_closed.is_seq_closed: a closed set is sequentially closed;
is_seq_closed.seq_closure_eq: sequential closure of a sequentially closed set s is equal to s;
seq_closure_eq_closure: in a Fréchet-Urysohn space, the sequential closure of a set is equal to its closure;
tendsto_nhds_iff_seq_tendsto, frechet_urysohn_space.of_seq_tendsto_imp_tendsto: a topological space is a Fréchet-Urysohn space if and only if sequential convergence implies convergence;
topological_space.first_countable_topology.frechet_urysohn_space: every topological space with first countable topology is a Fréchet-Urysohn space;
frechet_urysohn_space.to_sequential_space: every Fréchet-Urysohn space is a sequential space;
is_seq_compact.is_compact: a sequentially compact set in a uniform space with countably generated uniformity is compact.

Tags #

sequentially closed, sequentially compact, sequential space

Sequential closures, sequential continuity, and sequential spaces. #

source

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

seq_closure s = {a : X | ∃ (x : ℕ → X), (∀ (n : ℕ), x n ∈ s) ∧ filter.tendsto x filter.at_top (nhds a)}

source

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

s ⊆ seq_closure s

source

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

seq_closure s ⊆ closure s

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

source

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

is_seq_closed s = ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, (∀ (n : ℕ), x n ∈ s) → filter.tendsto x filter.at_top (nhds p) → p ∈ s

source

theorem is_seq_closed.seq_closure_eq {X : Type u_1} [topological_space X] {s : set X} (hs : is_seq_closed s) :

seq_closure s = s

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

source

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

is_seq_closed s

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

source

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

is_seq_closed s ↔ seq_closure s = s

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

source

@[protected]

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

is_seq_closed s

A set is sequentially closed if it is closed.

source

@[class]

structure frechet_urysohn_space (X : Type u_3) [topological_space X] :

Prop

closure_subset_seq_closure : ∀ (s : set X), closure s ⊆ seq_closure s

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

topological_space.first_countable_topology.frechet_urysohn_space

source

theorem seq_closure_eq_closure {X : Type u_1} [topological_space X] [frechet_urysohn_space X] (s : set X) :

seq_closure s = closure s

source

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.

source

theorem tendsto_nhds_iff_seq_tendsto {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] [frechet_urysohn_space X] {f : X → Y} {a : X} {b : Y} :

filter.tendsto f (nhds a) (nhds b) ↔ ∀ (u : ℕ → X), filter.tendsto u filter.at_top (nhds a) → filter.tendsto (f ∘ u) filter.at_top (nhds b)

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.

source

theorem frechet_urysohn_space.of_seq_tendsto_imp_tendsto {X : Type u_1} [topological_space X] (h : ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), filter.tendsto u filter.at_top (nhds a) → filter.tendsto (f ∘ u) filter.at_top (nhds (f a))) → continuous_at f a) :

frechet_urysohn_space X

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

source

@[protected, instance]

def topological_space.first_countable_topology.frechet_urysohn_space {X : Type u_1} [topological_space X] [topological_space.first_countable_topology X] :

frechet_urysohn_space X

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

source

@[class]

structure sequential_space (X : Type u_3) [topological_space X] :

Prop

is_closed_of_seq : ∀ (s : set X), is_seq_closed s → is_closed s

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

source

@[protected, instance]

def frechet_urysohn_space.to_sequential_space {X : Type u_1} [topological_space X] [frechet_urysohn_space X] :

sequential_space X

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

source

@[protected]

theorem is_seq_closed.is_closed {X : Type u_1} [topological_space X] [sequential_space X] {s : set X} (hs : is_seq_closed s) :

is_closed s

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

source

theorem is_seq_closed_iff_is_closed {X : Type u_1} [topological_space X] [sequential_space X] {M : set X} :

is_seq_closed M ↔ is_closed M

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

source

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

seq_continuous f = ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, filter.tendsto x filter.at_top (nhds p) → filter.tendsto (f ∘ x) filter.at_top (nhds (f p))

source

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) :

is_seq_closed (f ⁻¹' s)

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

source

@[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) :

seq_continuous f

source

@[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) :

continuous f

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

source

theorem continuous_iff_seq_continuous {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] [sequential_space X] {f : X → Y} :

continuous f ↔ seq_continuous f

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

source

theorem quotient_map.sequential_space {X : Type u_1} {Y : Type u_2} [topological_space X] [topological_space Y] [sequential_space X] {f : X → Y} (hf : quotient_map f) :

sequential_space Y

source

@[protected, instance]

def quotient.sequential_space {X : Type u_1} [topological_space X] [sequential_space X] {s : setoid X} :

sequential_space (quotient s)

The quotient of a sequential space is a sequential space.

source

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

is_seq_compact s = ∀ ⦃x : ℕ → X⦄, (∀ (n : ℕ), x n ∈ s) → (∃ (a : X) (H : a ∈ s) (φ : ℕ → ℕ), strict_mono φ ∧ filter.tendsto (x ∘ φ) filter.at_top (nhds a))

source

@[class]

structure seq_compact_space (X : Type u_3) [topological_space X] :

Prop

seq_compact_univ : is_seq_compact set.univ

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

Instances of this typeclass

first_countable_topology.seq_compact_of_compact

source

theorem seq_compact_space_iff (X : Type u_3) [topological_space X] :

seq_compact_space X ↔ is_seq_compact set.univ

source

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)

source

theorem seq_compact_space.tendsto_subseq {X : Type u_1} [topological_space X] [seq_compact_space X] (x : ℕ → X) :

∃ (a : X) (φ : ℕ → ℕ), strict_mono φ ∧ filter.tendsto (x ∘ φ) filter.at_top (nhds a)

source

@[protected]

theorem is_compact.is_seq_compact {X : Type u_1} [topological_space X] [topological_space.first_countable_topology X] {s : set X} (hs : is_compact s) :

is_seq_compact s

source

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)

source

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)

source

@[protected, instance]

def first_countable_topology.seq_compact_of_compact {X : Type u_1} [topological_space X] [topological_space.first_countable_topology X] [compact_space X] :

seq_compact_space X

source

theorem compact_space.tendsto_subseq {X : Type u_1} [topological_space X] [topological_space.first_countable_topology X] [compact_space X] (x : ℕ → X) :

∃ (a : X) (φ : ℕ → ℕ), strict_mono φ ∧ filter.tendsto (x ∘ φ) filter.at_top (nhds a)

source

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)

source

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)

source

@[protected]

theorem is_seq_compact.totally_bounded {X : Type u_1} [uniform_space X] {s : set X} (h : is_seq_compact s) :

totally_bounded s

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

source

@[protected]

theorem is_seq_compact.is_complete {X : Type u_1} [uniform_space X] {s : set X} [(uniformity X).is_countably_generated] (hs : is_seq_compact s) :

is_complete s

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

source

@[protected]

theorem is_seq_compact.is_compact {X : Type u_1} [uniform_space X] {s : set X} [(uniformity X).is_countably_generated] (hs : is_seq_compact s) :

is_compact s

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

source

@[protected]

theorem uniform_space.is_compact_iff_is_seq_compact {X : Type u_1} [uniform_space X] {s : set X} [(uniformity X).is_countably_generated] :

is_compact s ↔ is_seq_compact s

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.

source

theorem uniform_space.compact_space_iff_seq_compact_space {X : Type u_1} [uniform_space X] [(uniformity X).is_countably_generated] :

compact_space X ↔ seq_compact_space X

source

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)

source

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.

source

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.