# mathlibdocumentation

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. 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. #

theorem topological_space.seq_tendsto_iff {α : Type u_1} {x : → α} {limit : α} :
(𝓝 limit) ∀ (U : set α), limit U(∃ (N : ), ∀ (n : ), n Nx n U)

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

def sequential_closure {α : Type u_1} (M : 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
theorem subset_sequential_closure {α : Type u_1} (M : set α) :
def is_seq_closed {α : Type u_1} (s : 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
theorem is_seq_closed_of_def {α : Type u_1} {A : set α} (h : ∀ (x : → α) (p : α), (∀ (n : ), x n A) (𝓝 p)p A) :

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

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

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

theorem is_seq_closed_of_is_closed {α : Type u_1} (M : set α) (_x : is_closed M) :

A set is sequentially closed if it is closed.

theorem mem_of_is_seq_closed {α : Type u_1} {A : set α} (_x : is_seq_closed A) {x : → α} (_x_1 : ∀ (n : ), x n A) {limit : α} (_x_2 : (𝓝 limit)) :
limit A

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

theorem mem_of_is_closed_sequential {α : Type u_1} {A : set α} (_x : is_closed A) {x : → α} (_x_1 : ∀ (n : ), x n A) {limit : α} (_x_2 : (𝓝 limit)) :
limit A

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

@[class]
structure sequential_space (α : Type u_3)  :
Prop
• sequential_closure_eq_closure : ∀ (M : set α),

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
theorem is_seq_closed_iff_is_closed {α : Type u_1} {M : set α} :

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

theorem mem_closure_iff_seq_limit {α : Type u_1} {s : set α} {a : α} :
a ∃ (x : → α), (∀ (n : ), x n s) (𝓝 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.

def sequentially_continuous {α : Type u_1} {β : Type u_2} (f : α → β) :
Prop

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

Equations
theorem continuous.to_sequentially_continuous {α : Type u_1} {β : Type u_2} {f : α → β} (_x : continuous f) :
theorem continuous_iff_sequentially_continuous {α : Type u_1} {β : Type u_2} {f : α → β}  :

In a sequential space, continuity and sequential continuity coincide.

@[instance]

Every first-countable space is sequential.

def is_seq_compact {α : Type u_1} (s : set α) :
Prop

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

Equations
@[class]
structure seq_compact_space (α : Type u_3)  :
Prop
• seq_compact_univ :

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

Instances
theorem is_seq_compact.subseq_of_frequently_in {α : Type u_1} {s : set α} (hs : is_seq_compact s) {u : → α} (hu : ∃ᶠ (n : ) in filter.at_top, u n s) :
∃ (x : α) (H : x s) (φ : ), filter.tendsto (u φ) filter.at_top (𝓝 x)
theorem seq_compact_space.tendsto_subseq {α : Type u_1} (u : → α) :
∃ (x : α) (φ : ), filter.tendsto (u φ) filter.at_top (𝓝 x)
theorem is_compact.is_seq_compact {α : Type u_1} {s : set α} (hs : is_compact s) :
theorem is_compact.tendsto_subseq' {α : Type u_1} {s : set α} {u : → α} (hs : is_compact s) (hu : ∃ᶠ (n : ) in filter.at_top, u n s) :
∃ (x : α) (H : x s) (φ : ), filter.tendsto (u φ) filter.at_top (𝓝 x)
theorem is_compact.tendsto_subseq {α : Type u_1} {s : set α} {u : → α} (hs : is_compact s) (hu : ∀ (n : ), u n s) :
∃ (x : α) (H : x s) (φ : ), filter.tendsto (u φ) filter.at_top (𝓝 x)
@[instance]
theorem compact_space.tendsto_subseq {α : Type u_1} (u : → α) :
∃ (x : α) (φ : ), filter.tendsto (u φ) filter.at_top (𝓝 x)
theorem lebesgue_number_lemma_seq {β : Type u_2} {s : set β} {ι : Type u_1} [(𝓤 β).is_countably_generated] {c : ι → set β} (hs : is_seq_compact s) (hc₁ : ∀ (i : ι), is_open (c i)) (hc₂ : s ⋃ (i : ι), c i) :
∃ (V : set × β)) (H : V 𝓤 β), ∀ (x : β), x s(∃ (i : ι), c i)
theorem is_seq_compact.totally_bounded {β : Type u_2} {s : set β} (h : is_seq_compact s) :
theorem is_seq_compact.is_compact {β : Type u_2} {s : set β} [(𝓤 β).is_countably_generated] (hs : is_seq_compact s) :
theorem uniform_space.compact_iff_seq_compact {β : Type u_2} {s : set β} [(𝓤 β).is_countably_generated] :

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 tendsto_subseq_of_frequently_bounded {β : Type u_2} [metric_space β] {s : set β} [proper_space β] (hs : metric.bounded s) {u : → β} (hu : ∃ᶠ (n : ) in filter.at_top, u n s) :
∃ (b : β) (H : b closure s) (φ : ), filter.tendsto (u φ) filter.at_top (𝓝 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.

theorem tendsto_subseq_of_bounded {β : Type u_2} [metric_space β] {s : set β} [proper_space β] (hs : metric.bounded s) {u : → β} (hu : ∀ (n : ), u n s) :
∃ (b : β) (H : b closure s) (φ : ), filter.tendsto (u φ) filter.at_top (𝓝 b)

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

theorem seq_compact.lebesgue_number_lemma_of_metric {β : Type u_2} [metric_space β] {s : set β} {ι : Type u_1} {c : ι → set β} (hs : is_seq_compact s) (hc₁ : ∀ (i : ι), is_open (c i)) (hc₂ : s ⋃ (i : ι), c i) :
∃ (δ : ) (H : δ > 0), ∀ (x : β), x s(∃ (i : ι), δ c i)