Documentation

Mathlib.Topology.Defs.Filter

Definitions about filters in topological spaces #

In this file we define filters in topological spaces, as well as other definitions that rely on Filters.

Main Definitions #

Neighborhoods filter #

Continuity at a point #

Limits #

Cluster points and accumulation points #

Notations #

@[irreducible]
def nhds {X : Type u_3} [TopologicalSpace X] (x : X) :

A set is called a neighborhood of x if it contains an open set around x. The set of all neighborhoods of x forms a filter, the neighborhood filter at x, is here defined as the infimum over the principal filters of all open sets containing x.

Equations
    Instances For
      theorem nhds_def {X : Type u_3} [TopologicalSpace X] (x : X) :
      nhds x = ⹅ s ∈ {s : Set X | x ∈ s ∧ IsOpen s}, Filter.principal s

      A set is called a neighborhood of x if it contains an open set around x. The set of all neighborhoods of x forms a filter, the neighborhood filter at x, is here defined as the infimum over the principal filters of all open sets containing x.

      Equations
        Instances For
          def nhdsWithin {X : Type u_1} [TopologicalSpace X] (x : X) (s : Set X) :

          The "neighborhood within" filter. Elements of 𝓝[s] x are sets containing the intersection of s and a neighborhood of x.

          Equations
            Instances For

              The "neighborhood within" filter. Elements of 𝓝[s] x are sets containing the intersection of s and a neighborhood of x.

              Equations
                Instances For

                  Pretty printer defined by notation3 command.

                  Equations
                    Instances For

                      Notation for the filter of punctured neighborhoods of a point.

                      Equations
                        Instances For

                          Pretty printer defined by notation3 command.

                          Equations
                            Instances For

                              Notation for the filter of right neighborhoods of a point.

                              Equations
                                Instances For

                                  Pretty printer defined by notation3 command.

                                  Equations
                                    Instances For

                                      Notation for the filter of left neighborhoods of a point.

                                      Equations
                                        Instances For

                                          Notation for the filter of punctured right neighborhoods of a point.

                                          Equations
                                            Instances For

                                              Pretty printer defined by notation3 command.

                                              Equations
                                                Instances For

                                                  Notation for the filter of punctured left neighborhoods of a point.

                                                  Equations
                                                    Instances For

                                                      Pretty printer defined by notation3 command.

                                                      Equations
                                                        Instances For
                                                          def nhdsSet {X : Type u_1} [TopologicalSpace X] (s : Set X) :

                                                          The filter of neighborhoods of a set in a topological space.

                                                          Equations
                                                            Instances For

                                                              The filter of neighborhoods of a set in a topological space.

                                                              Equations
                                                                Instances For
                                                                  def exterior {X : Type u_1} [TopologicalSpace X] (s : Set X) :
                                                                  Set X

                                                                  The exterior of a set is the intersection of all its neighborhoods. In an Alexandrov-discrete space, this is the smallest neighborhood of the set.

                                                                  Note that this construction is unnamed in the literature. We choose the name in analogy to interior.

                                                                  Equations
                                                                    Instances For
                                                                      def ContinuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (x : X) :

                                                                      A function between topological spaces is continuous at a point x₀ if f x tends to f x₀ when x tends to x₀.

                                                                      Equations
                                                                        Instances For
                                                                          def ContinuousWithinAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (s : Set X) (x : X) :

                                                                          A function between topological spaces is continuous at a point x₀ within a subset s if f x tends to f x₀ when x tends to x₀ while staying within s.

                                                                          Equations
                                                                            Instances For
                                                                              def ContinuousOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (s : Set X) :

                                                                              A function between topological spaces is continuous on a subset s when it's continuous at every point of s within s.

                                                                              Equations
                                                                                Instances For
                                                                                  def Specializes {X : Type u_1} [TopologicalSpace X] (x y : X) :

                                                                                  x specializes to y (notation: x ″ y) if either of the following equivalent properties hold:

                                                                                  • 𝓝 x ≀ 𝓝 y; this property is used as the definition;
                                                                                  • pure x ≀ 𝓝 y; in other words, any neighbourhood of y contains x;
                                                                                  • y ∈ closure {x};
                                                                                  • closure {y} ⊆ closure {x};
                                                                                  • for any closed set s we have x ∈ s → y ∈ s;
                                                                                  • for any open set s we have y ∈ s → x ∈ s;
                                                                                  • y is a cluster point of the filter pure x = 𝓟 {x}.

                                                                                  This relation defines a Preorder on X. If X is a T₀ space, then this preorder is a partial order. If X is a T₁ space, then this partial order is trivial : x ″ y ↔ x = y.

                                                                                  Equations
                                                                                    Instances For

                                                                                      x specializes to y (notation: x ″ y) if either of the following equivalent properties hold:

                                                                                      • 𝓝 x ≀ 𝓝 y; this property is used as the definition;
                                                                                      • pure x ≀ 𝓝 y; in other words, any neighbourhood of y contains x;
                                                                                      • y ∈ closure {x};
                                                                                      • closure {y} ⊆ closure {x};
                                                                                      • for any closed set s we have x ∈ s → y ∈ s;
                                                                                      • for any open set s we have y ∈ s → x ∈ s;
                                                                                      • y is a cluster point of the filter pure x = 𝓟 {x}.

                                                                                      This relation defines a Preorder on X. If X is a T₀ space, then this preorder is a partial order. If X is a T₁ space, then this partial order is trivial : x ″ y ↔ x = y.

                                                                                      Equations
                                                                                        Instances For
                                                                                          def Inseparable {X : Type u_1} [TopologicalSpace X] (x y : X) :

                                                                                          Two points x and y in a topological space are Inseparable if any of the following equivalent properties hold:

                                                                                          • 𝓝 x = 𝓝 y; we use this property as the definition;
                                                                                          • for any open set s, x ∈ s ↔ y ∈ s, see inseparable_iff_forall_isOpen;
                                                                                          • for any closed set s, x ∈ s ↔ y ∈ s, see inseparable_iff_forall_isClosed;
                                                                                          • x ∈ closure {y} and y ∈ closure {x}, see inseparable_iff_mem_closure;
                                                                                          • closure {x} = closure {y}, see inseparable_iff_closure_eq.
                                                                                          Equations
                                                                                            Instances For

                                                                                              Specialization forms a preorder on the topological space.

                                                                                              Equations
                                                                                                Instances For

                                                                                                  A setoid version of Inseparable, used to define the SeparationQuotient.

                                                                                                  Equations
                                                                                                    Instances For

                                                                                                      The quotient of a topological space by its inseparableSetoid. This quotient is guaranteed to be a T₀ space.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          noncomputable def lim {X : Type u_1} [TopologicalSpace X] [Nonempty X] (f : Filter X) :
                                                                                                          X

                                                                                                          If f is a filter, then Filter.lim f is a limit of the filter, if it exists.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              noncomputable def limUnder {X : Type u_1} [TopologicalSpace X] {α : Type u_3} [Nonempty X] (f : Filter α) (g : α → X) :
                                                                                                              X

                                                                                                              If f is a filter in α and g : α → X is a function, then limUnder f g is a limit of g at f, if it exists.

                                                                                                              Equations
                                                                                                                Instances For
                                                                                                                  def ClusterPt {X : Type u_1} [TopologicalSpace X] (x : X) (F : Filter X) :

                                                                                                                  A point x is a cluster point of a filter F if 𝓝 x ⊓ F ≠ ⊄. Also known as an accumulation point or a limit point, but beware that terminology varies. This is not the same as asking 𝓝[≠] x ⊓ F ≠ ⊄, which is called AccPt in Mathlib. See mem_closure_iff_clusterPt in particular.

                                                                                                                  Equations
                                                                                                                    Instances For
                                                                                                                      def MapClusterPt {X : Type u_1} [TopologicalSpace X] {Îč : Type u_3} (x : X) (F : Filter Îč) (u : Îč → X) :

                                                                                                                      A point x is a cluster point of a sequence u along a filter F if it is a cluster point of map u F.

                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          def AccPt {X : Type u_1} [TopologicalSpace X] (x : X) (F : Filter X) :

                                                                                                                          A point x is an accumulation point of a filter F if 𝓝[≠] x ⊓ F ≠ ⊄. See also ClusterPt.

                                                                                                                          Equations
                                                                                                                            Instances For
                                                                                                                              def IsCompact {X : Type u_1} [TopologicalSpace X] (s : Set X) :

                                                                                                                              A set s is compact if for every nontrivial filter f that contains s, there exists a ∈ s such that every set of f meets every neighborhood of a.

                                                                                                                              Equations
                                                                                                                                Instances For
                                                                                                                                  class CompactSpace (X : Type u_1) [TopologicalSpace X] :

                                                                                                                                  Type class for compact spaces. Separation is sometimes included in the definition, especially in the French literature, but we do not include it here.

                                                                                                                                  Instances

                                                                                                                                    X is a noncompact topological space if it is not a compact space.

                                                                                                                                    Instances

                                                                                                                                      We say that a topological space is a weakly locally compact space, if each point of this space admits a compact neighborhood.

                                                                                                                                      • exists_compact_mem_nhds (x : X) : ∃ (s : Set X), IsCompact s ∧ s ∈ nhds x

                                                                                                                                        Every point of a weakly locally compact space admits a compact neighborhood.

                                                                                                                                      Instances

                                                                                                                                        There are various definitions of "locally compact space" in the literature, which agree for Hausdorff spaces but not in general. This one is the precise condition on X needed for the evaluation map C(X, Y) × X → Y to be continuous for all Y when C(X, Y) is given the compact-open topology.

                                                                                                                                        See also WeaklyLocallyCompactSpace, a typeclass that only assumes that each point has a compact neighborhood.

                                                                                                                                        • local_compact_nhds (x : X) (n : Set X) : n ∈ nhds x → ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s

                                                                                                                                          In a locally compact space, every neighbourhood of every point contains a compact neighbourhood of that same point.

                                                                                                                                        Instances

                                                                                                                                          We say that X and Y are a locally compact pair of topological spaces, if for any continuous map f : X → Y, a point x : X, and a neighbourhood s ∈ 𝓝 (f x), there exists a compact neighbourhood K ∈ 𝓝 x such that f maps K to s.

                                                                                                                                          This is a technical assumption that appears in several theorems, most notably in ContinuousMap.continuous_comp' and ContinuousMap.continuous_eval. It is satisfied in two cases:

                                                                                                                                          • if X is a locally compact topological space, for obvious reasons;
                                                                                                                                          • if X is a weakly locally compact topological space and Y is an R₁ space; this fact is a simple generalization of the theorem saying that a weakly locally compact R₁ topological space is locally compact.
                                                                                                                                          • exists_mem_nhds_isCompact_mapsTo {f : X → Y} {x : X} {s : Set Y} : Continuous f → s ∈ nhds (f x) → ∃ K ∈ nhds x, IsCompact K ∧ Set.MapsTo f K s

                                                                                                                                            If f : X → Y is a continuous map in a locally compact pair of topological spaces and s : Set Y is a neighbourhood of f x, x : X, then there exists a compact neighbourhood K of x such that f maps K to s.

                                                                                                                                          Instances

                                                                                                                                            Filter.cocompact is the filter generated by complements to compact sets.

                                                                                                                                            Equations
                                                                                                                                              Instances For

                                                                                                                                                Filter.coclosedCompact is the filter generated by complements to closed compact sets. In a Hausdorff space, this is the same as Filter.cocompact.

                                                                                                                                                Equations
                                                                                                                                                  Instances For