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

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