Sequences in topological spaces

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

define the sequential closure of a set and prove that it's contained in the closure,
define a type class "sequential_space" in which closure and sequential closure agree,
define sequential continuity and show that it coincides with continuity in sequential spaces,
provide an instance that shows that every first-countable (and in particular metric) space is a sequential space.
define sequential compactness, prove that compactness implies sequential compactness in first countable spaces, and prove they are equivalent for uniform spaces having a countable uniformity basis (in particular metric spaces).

Sequential closures, sequential continuity, and sequential spaces.

source

theorem topological_space.seq_tendsto_iff {α : Type u_1} [topological_space α] {x : ℕ → α} {limit : α} :

filter.tendsto x filter.at_top (nhds limit) ↔ ∀ (U : set α), limit ∈ U → is_open U → (∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → x n ∈ U)

A sequence converges in the sence of topological spaces iff the associated statement for filter holds.

source

def sequential_closure {α : Type u_1} [topological_space α] :

set α → set α

The sequential closure of a subset M ⊆ α of a topological space α is the set of all p ∈ α which arise as limit of sequences in M.

Equations

sequential_closure M = {p : α | ∃ (x : ℕ → α), (∀ (n : ℕ), x n ∈ M) ∧ filter.tendsto x filter.at_top (nhds p)}

source

theorem subset_sequential_closure {α : Type u_1} [topological_space α] (M : set α) :

M ⊆ sequential_closure M

source

def is_seq_closed {α : Type u_1} [topological_space α] :

set α → 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.

Equations

is_seq_closed s = (s = sequential_closure s)

source

theorem is_seq_closed_of_def {α : Type u_1} [topological_space α] {A : set α} :

(∀ (x : ℕ → α) (p : α), (∀ (n : ℕ), x n ∈ A) → filter.tendsto x filter.at_top (nhds p) → p ∈ A) → is_seq_closed A

A convenience lemma for showing that a set is sequentially closed.

source

theorem sequential_closure_subset_closure {α : Type u_1} [topological_space α] (M : set α) :

sequential_closure M ⊆ closure M

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

source

theorem is_seq_closed_of_is_closed {α : Type u_1} [topological_space α] (M : set α) :

is_closed M → is_seq_closed M

A set is sequentially closed if it is closed.

source

theorem mem_of_is_seq_closed {α : Type u_1} [topological_space α] {A : set α} (_x : is_seq_closed A) {x : ℕ → α} (_x_1 : ∀ (n : ℕ), x n ∈ A) {limit : α} :

filter.tendsto x filter.at_top (nhds limit) → limit ∈ A

The limit of a convergent sequence in a sequentially closed set is in that set.

source

theorem mem_of_is_closed_sequential {α : Type u_1} [topological_space α] {A : set α} (_x : is_closed A) {x : ℕ → α} (_x_1 : ∀ (n : ℕ), x n ∈ A) {limit : α} :

filter.tendsto x filter.at_top (nhds limit) → limit ∈ A

The limit of a convergent sequence in a closed set is in that set.

source

@[class]

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

Prop

sequential_closure_eq_closure : ∀ (M : set α), sequential_closure M = closure M

A sequential space is a space in which 'sequences are enough to probe the topology'. This can be formalised by demanding that the sequential closure and the closure coincide. The following statements show that other topological properties can be deduced from sequences in sequential spaces.

Instances

topological_space.first_countable_topology.sequential_space

source

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

is_seq_closed M ↔ is_closed M

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

source

theorem mem_closure_iff_seq_limit {α : Type u_1} [topological_space α] [sequential_space α] {s : set α} {a : α} :

a ∈ closure s ↔ ∃ (x : ℕ → α), (∀ (n : ℕ), x n ∈ s) ∧ filter.tendsto x filter.at_top (nhds a)

In a sequential space, a point belongs to the closure of a set iff it is a limit of a sequence taking values in this set.

source

def sequentially_continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

(α → β) → Prop

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

Equations

sequentially_continuous f = ∀ (x : ℕ → α) {limit : α}, filter.tendsto x filter.at_top (nhds limit) → filter.tendsto (f ∘ x) filter.at_top (nhds (f limit))

source

theorem continuous.to_sequentially_continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :

continuous f → sequentially_continuous f

source

theorem continuous_iff_sequentially_continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} [sequential_space α] :

continuous f ↔ sequentially_continuous f

In a sequential space, continuity and sequential continuity coincide.

source

@[instance]

def topological_space.first_countable_topology.sequential_space {α : Type u_1} [topological_space α] [topological_space.first_countable_topology α] :

sequential_space α

Every first-countable space is sequential.

Equations

source

def is_seq_compact {α : Type u_1} [topological_space α] :

set α → Prop

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

Equations

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

source

@[class]

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

Prop

seq_compact_univ : is_seq_compact set.univ

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

Instances

first_countable_topology.seq_compact_of_compact

source

theorem is_seq_compact.subseq_of_frequently_in {α : Type u_1} [topological_space α] {s : set α} (hs : is_seq_compact s) {u : ℕ → α} :

(∃ᶠ (n : ℕ) in filter.at_top, u n ∈ s) → (∃ (x : α) (H : x ∈ s) (φ : ℕ → ℕ), strict_mono φ ∧ filter.tendsto (u ∘ φ) filter.at_top (nhds x))

source

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

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

source

theorem is_compact.is_seq_compact {α : Type u_1} [topological_space α] [topological_space.first_countable_topology α] {s : set α} :

is_compact s → is_seq_compact s

source

theorem is_compact.tendsto_subseq' {α : Type u_1} [topological_space α] [topological_space.first_countable_topology α] {s : set α} {u : ℕ → α} :

is_compact s → (∃ᶠ (n : ℕ) in filter.at_top, u n ∈ s) → (∃ (x : α) (H : x ∈ s) (φ : ℕ → ℕ), strict_mono φ ∧ filter.tendsto (u ∘ φ) filter.at_top (nhds x))

source

theorem is_compact.tendsto_subseq {α : Type u_1} [topological_space α] [topological_space.first_countable_topology α] {s : set α} {u : ℕ → α} :

is_compact s → (∀ (n : ℕ), u n ∈ s) → (∃ (x : α) (H : x ∈ s) (φ : ℕ → ℕ), strict_mono φ ∧ filter.tendsto (u ∘ φ) filter.at_top (nhds x))

source

@[instance]

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

seq_compact_space α

Equations

first_countable_topology.seq_compact_of_compact = _

source

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

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

source

theorem lebesgue_number_lemma_seq {β : Type u_2} [uniform_space β] {s : set β} {ι : Type u_1} {c : ι → set β} :

is_seq_compact s → (∀ (i : ι), is_open (c i)) → (s ⊆ ⋃ (i : ι), c i) → (uniformity β).is_countably_generated → (∃ (V : set (β × β)) (H : V ∈ uniformity β), symmetric_rel V ∧ ∀ (x : β), x ∈ s → (∃ (i : ι), uniform_space.ball x V ⊆ c i))

source

theorem is_seq_compact.totally_bounded {β : Type u_2} [uniform_space β] {s : set β} :

is_seq_compact s → totally_bounded s

source

theorem is_seq_compact.is_compact {β : Type u_2} [uniform_space β] {s : set β} :

(uniformity β).is_countably_generated → is_seq_compact s → is_compact s

source

theorem uniform_space.compact_iff_seq_compact {β : Type u_2} [uniform_space β] {s : set β} :

(uniformity β).is_countably_generated → (is_compact s ↔ is_seq_compact s)

source

theorem uniform_space.compact_space_iff_seq_compact_space {β : Type u_2} [uniform_space β] :

(uniformity β).is_countably_generated → (compact_space β ↔ seq_compact_space β)

source

theorem metric.compact_iff_seq_compact {β : Type u_2} [metric_space β] {s : set β} :

is_compact s ↔ is_seq_compact s

A version of Bolzano-Weistrass: in a metric space, is_compact s ↔ is_seq_compact s

source

theorem tendsto_subseq_of_frequently_bounded {β : Type u_2} [metric_space β] {s : set β} [proper_space β] (hs : metric.bounded s) {u : ℕ → β} :

(∃ᶠ (n : ℕ) in filter.at_top, u n ∈ s) → (∃ (b : β) (H : b ∈ closure s) (φ : ℕ → ℕ), strict_mono φ ∧ filter.tendsto (u ∘ φ) filter.at_top (nhds b))

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 {β : Type u_2} [metric_space β] {s : set β} [proper_space β] (hs : metric.bounded s) {u : ℕ → β} :

(∀ (n : ℕ), u n ∈ s) → (∃ (b : β) (H : b ∈ closure s) (φ : ℕ → ℕ), strict_mono φ ∧ filter.tendsto (u ∘ φ) filter.at_top (nhds b))

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

source

theorem metric.compact_space_iff_seq_compact_space {β : Type u_2} [metric_space β] :

compact_space β ↔ seq_compact_space β

source

theorem seq_compact.lebesgue_number_lemma_of_metric {β : Type u_2} [metric_space β] {s : set β} {ι : Type u_1} {c : ι → set β} :

is_seq_compact s → (∀ (i : ι), is_open (c i)) → (s ⊆ ⋃ (i : ι), c i) → (∃ (δ : ℝ) (H : δ > 0), ∀ (x : β), x ∈ s → (∃ (i : ι), metric.ball x δ ⊆ c i))

mathlib documentation

topology.sequences

Sequences in topological spaces

Sequential closures, sequential continuity, and sequential spaces.

General documentation

Additional documentation

Library

mathlib documentation

topology.​sequences

Sequences in topological spaces

Sequential closures, sequential continuity, and sequential spaces.

General documentation

Additional documentation

Library

topology.sequences