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

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

Main results

• seqClosure_subset_closure: closure of a set includes its sequential closure;
• IsClosed.isSeqClosed: a closed set is sequentially closed;
• IsSeqClosed.seqClosure_eq: sequential closure of a sequentially closed set s is equal to s;
• seqClosure_eq_closure: in a Fréchet-Urysohn space, the sequential closure of a set is equal to its closure;
• tendsto_nhds_iff_seq_tendsto, FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto: a topological space is a Fréchet-Urysohn space if and only if sequential convergence implies convergence;
• FirstCountableTopology.frechetUrysohnSpace: every topological space with first countable topology is a Fréchet-Urysohn space;
• FrechetUrysohnSpace.to_sequentialSpace: every Fréchet-Urysohn space is a sequential space;
• IsSeqCompact.isCompact: 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.

def seqClosure {X : Type u_1} [TopologicalSpace 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

• seqClosure s = {a : X | ∃ (x : ℕ → X), (∀ (n : ℕ), x n ∈ s) ∧ Filter.Tendsto x Filter.atTop (nhds a)}

theorem subset_seqClosure {X : Type u_1} [TopologicalSpace X] {s : Set X} : s ⊆ seqClosure s

theorem seqClosure_subset_closure {X : Type u_1} [TopologicalSpace X] {s : Set X} : seqClosure s ⊆ closure s

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

def IsSeqClosed {X : Type u_1} [TopologicalSpace 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

• IsSeqClosed s = ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, (∀ (n : ℕ), x n ∈ s) → Filter.Tendsto x Filter.atTop (nhds p) → p ∈ s

theorem IsSeqClosed.seqClosure_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsSeqClosed s) : seqClosure s = s

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

theorem isSeqClosed_of_seqClosure_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : seqClosure s = s) : IsSeqClosed s

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

theorem isSeqClosed_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsSeqClosed s ↔ seqClosure s = s

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

theorem IsClosed.isSeqClosed {X : Type u_1} [TopologicalSpace X] {s : Set X} (hc : IsClosed s) : IsSeqClosed s

A set is sequentially closed if it is closed.

class FrechetUrysohnSpace (X : Type u_3) [TopologicalSpace 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.

• closure_subset_seqClosure : ∀ (s : Set X), closure s ⊆ seqClosure s

theorem seqClosure_eq_closure {X : Type u_1} [TopologicalSpace X] [FrechetUrysohnSpace X] (s : Set X) : seqClosure s = closure s

theorem mem_closure_iff_seq_limit {X : Type u_1} [TopologicalSpace X] [FrechetUrysohnSpace X] {s : Set X} {a : X} : a ∈ closure s ↔ ∃ (x : ℕ → X), (∀ (n : ℕ), x n ∈ s) ∧ Filter.Tendsto x Filter.atTop (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.

theorem tendsto_nhds_iff_seq_tendsto {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [FrechetUrysohnSpace X] {f : X → Y} {a : X} {b : Y} : Filter.Tendsto f (nhds a) (nhds b) ↔ ∀ (u : ℕ → X), Filter.Tendsto u Filter.atTop (nhds a) → Filter.Tendsto (f ∘ u) Filter.atTop (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 FrechetUrysohnSpace, see FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto.

theorem FrechetUrysohnSpace.of_seq_tendsto_imp_tendsto {X : Type u_1} [TopologicalSpace X] (h : ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Filter.Tendsto u Filter.atTop (nhds a) → Filter.Tendsto (f ∘ u) Filter.atTop (nhds (f a))) → ContinuousAt f a) : FrechetUrysohnSpace X

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

instance FirstCountableTopology.frechetUrysohnSpace {X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] : FrechetUrysohnSpace X

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

Equations

• (_ : FrechetUrysohnSpace X) = (_ : FrechetUrysohnSpace X)

class SequentialSpace (X : Type u_3) [TopologicalSpace 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.

• isClosed_of_seq : ∀ (s : Set X), IsSeqClosed s → IsClosed s

instance FrechetUrysohnSpace.to_sequentialSpace {X : Type u_1} [TopologicalSpace X] [FrechetUrysohnSpace X] : SequentialSpace X

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

Equations

• (_ : SequentialSpace X) = (_ : SequentialSpace X)

theorem IsSeqClosed.isClosed {X : Type u_1} [TopologicalSpace X] [SequentialSpace X] {s : Set X} (hs : IsSeqClosed s) : IsClosed s

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

theorem isSeqClosed_iff_isClosed {X : Type u_1} [TopologicalSpace X] [SequentialSpace X] {M : Set X} : IsSeqClosed M ↔ IsClosed M

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

def SeqContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop

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

Equations

• SeqContinuous f = ∀ ⦃x : ℕ → X⦄ ⦃p : X⦄, Filter.Tendsto x Filter.atTop (nhds p) → Filter.Tendsto (f ∘ x) Filter.atTop (nhds (f p))

theorem IsSeqClosed.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set Y} (hs : IsSeqClosed s) (hf : SeqContinuous f) : IsSeqClosed (f ⁻¹' s)

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

theorem Continuous.seqContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) : SeqContinuous f

theorem SeqContinuous.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SequentialSpace X] {f : X → Y} (hf : SeqContinuous f) : Continuous f

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

theorem continuous_iff_seqContinuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SequentialSpace X] {f : X → Y} : Continuous f ↔ SeqContinuous f

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

theorem QuotientMap.sequentialSpace {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SequentialSpace X] {f : X → Y} (hf : QuotientMap f) : SequentialSpace Y

instance instSequentialSpaceQuotientInstTopologicalSpaceQuotient {X : Type u_1} [TopologicalSpace X] [SequentialSpace X] {s : Setoid X} : SequentialSpace (Quotient s)

The quotient of a sequential space is a sequential space.

Equations

• (_ : SequentialSpace (Quotient s)) = (_ : SequentialSpace (Quot Setoid.r))

def IsSeqCompact {X : Type u_1} [TopologicalSpace X] (s : Set X) : Prop

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

Equations

• IsSeqCompact s = ∀ ⦃x : ℕ → X⦄, (∀ (n : ℕ), x n ∈ s) → ∃ a ∈ s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

theorem seqCompactSpace_iff (X : Type u_3) [TopologicalSpace X] : SeqCompactSpace X ↔ IsSeqCompact Set.univ

class SeqCompactSpace (X : Type u_3) [TopologicalSpace X] : Prop

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

• seq_compact_univ : IsSeqCompact Set.univ

theorem IsSeqCompact.subseq_of_frequently_in {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsSeqCompact s) {x : ℕ → X} (hx : ∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) : ∃ a ∈ s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

theorem SeqCompactSpace.tendsto_subseq {X : Type u_1} [TopologicalSpace X] [SeqCompactSpace X] (x : ℕ → X) : ∃ (a : X) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

theorem IsCompact.isSeqCompact {X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] {s : Set X} (hs : IsCompact s) : IsSeqCompact s

theorem IsCompact.tendsto_subseq' {X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] {s : Set X} {x : ℕ → X} (hs : IsCompact s) (hx : ∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) : ∃ a ∈ s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

theorem IsCompact.tendsto_subseq {X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] {s : Set X} {x : ℕ → X} (hs : IsCompact s) (hx : ∀ (n : ℕ), x n ∈ s) : ∃ a ∈ s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

instance FirstCountableTopology.seq_compact_of_compact {X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] [CompactSpace X] : SeqCompactSpace X

Equations

• (_ : SeqCompactSpace X) = (_ : SeqCompactSpace X)

theorem CompactSpace.tendsto_subseq {X : Type u_1} [TopologicalSpace X] [FirstCountableTopology X] [CompactSpace X] (x : ℕ → X) : ∃ (a : X) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

theorem IsSeqCompact.exists_tendsto_of_frequently_mem {X : Type u_1} [UniformSpace X] {s : Set X} (hs : IsSeqCompact s) {u : ℕ → X} (hu : ∃ᶠ (n : ℕ) in Filter.atTop, u n ∈ s) (huc : CauchySeq u) : ∃ x ∈ s, Filter.Tendsto u Filter.atTop (nhds x)

theorem IsSeqCompact.exists_tendsto {X : Type u_1} [UniformSpace X] {s : Set X} (hs : IsSeqCompact s) {u : ℕ → X} (hu : ∀ (n : ℕ), u n ∈ s) (huc : CauchySeq u) : ∃ x ∈ s, Filter.Tendsto u Filter.atTop (nhds x)

theorem IsSeqCompact.totallyBounded {X : Type u_1} [UniformSpace X] {s : Set X} (h : IsSeqCompact s) : TotallyBounded s

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

theorem IsSeqCompact.isComplete {X : Type u_1} [UniformSpace X] {s : Set X} [Filter.IsCountablyGenerated (uniformity X)] (hs : IsSeqCompact s) : IsComplete s

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

theorem IsSeqCompact.isCompact {X : Type u_1} [UniformSpace X] {s : Set X} [Filter.IsCountablyGenerated (uniformity X)] (hs : IsSeqCompact s) : IsCompact s

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

theorem UniformSpace.isCompact_iff_isSeqCompact {X : Type u_1} [UniformSpace X] {s : Set X} [Filter.IsCountablyGenerated (uniformity X)] : IsCompact s ↔ IsSeqCompact 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.

theorem UniformSpace.compactSpace_iff_seqCompactSpace {X : Type u_1} [UniformSpace X] [Filter.IsCountablyGenerated (uniformity X)] : CompactSpace X ↔ SeqCompactSpace X

theorem SeqCompact.lebesgue_number_lemma_of_metric {X : Type u_1} [PseudoMetricSpace X] {ι : Sort u_3} {c : ι → Set X} {s : Set X} (hs : IsSeqCompact s) (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : s ⊆ ⋃ (i : ι), c i) : ∃ δ > 0, ∀ a ∈ s, ∃ (i : ι), Metric.ball a δ ⊆ c i

theorem tendsto_subseq_of_frequently_bounded {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : Bornology.IsBounded s) {x : ℕ → X} (hx : ∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) : ∃ a ∈ closure s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (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} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : Bornology.IsBounded s) {x : ℕ → X} (hx : ∀ (n : ℕ), x n ∈ s) : ∃ a ∈ closure s, ∃ (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

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