Documentation

Mathlib.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 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
Instances For
    theorem subset_seqClosure {X : Type u_1} [TopologicalSpace X] {s : Set X} :

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

    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
    Instances For
      theorem IsSeqClosed.seqClosure_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsSeqClosed 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) :

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

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

      A set is sequentially closed if it is closed.

      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
        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 : XY} {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 : XProp) (a : X), (∀ (u : X), Filter.Tendsto u Filter.atTop (nhds a)Filter.Tendsto (f u) Filter.atTop (nhds (f a)))ContinuousAt f a) :

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

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

        Equations

        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

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

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

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

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

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

          Equations
          Instances For
            theorem IsSeqClosed.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set Y} (hs : IsSeqClosed s) (hf : SeqContinuous f) :

            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 : XY} (hf : Continuous f) :
            theorem SeqContinuous.continuous {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [SequentialSpace X] {f : XY} (hf : SeqContinuous 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.

            The quotient of a sequential space is a sequential space.

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

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

            Equations
            Instances For

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

              Instances
                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.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)
                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)

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

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

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

                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 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, as, ∃ (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.