Documentation

Mathlib.Topology.Defs.Sequences

Sequences in topological spaces #

In this file we define sequential closure, continuity, compactness etc.

Main definitions #

Set operation #

Predicates #

Type classes #

Tags #

sequentially closed, sequentially compact, sequential space

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
    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
      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
        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 SeqCompactSpace.isSeqCompact_univ {X : Type u_1} :
            ∀ {inst : TopologicalSpace X} [self : SeqCompactSpace X], IsSeqCompact Set.univ
            @[deprecated SeqCompactSpace.isSeqCompact_univ]
            theorem seq_compact_univ {X : Type u_1} :
            ∀ {inst : TopologicalSpace X} [self : SeqCompactSpace X], IsSeqCompact Set.univ

            Alias of SeqCompactSpace.isSeqCompact_univ.

            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

              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
                theorem SequentialSpace.isClosed_of_seq {X : Type u_1} :
                ∀ {inst : TopologicalSpace X} [self : SequentialSpace X] (s : Set X), IsSeqClosed sIsClosed s
                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.