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
        • One or more equations did not get rendered due to their size.
        Instances For

          Notation for the filter of punctured neighborhoods of a point.

          Equations
          Instances For

            Pretty printer defined by notation3 command.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Notation for the filter of right neighborhoods of a point.

              Equations
              Instances For

                Pretty printer defined by notation3 command.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Pretty printer defined by notation3 command.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  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
                        • One or more equations did not get rendered due to their size.
                        Instances For

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

                          Equations
                          Instances For

                            Pretty printer defined by notation3 command.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            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 ContinuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : XY) (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 : XY) (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 : XY) (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 : 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 : 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_open;
                                            • for any closed set s, x ∈ s ↔ y ∈ s, see inseparable_iff_closed;
                                            • 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 Ultrafilter.lim {X : Type u_1} [TopologicalSpace X] (F : Ultrafilter X) :
                                                      X

                                                      If F is an ultrafilter, then Filter.Ultrafilter.lim F is a limit of the filter, if it exists. Note that dot notation F.lim can be used for F : Filter.Ultrafilter X.

                                                      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
                                                                    theorem CompactSpace.isCompact_univ {X : Type u_1} [TopologicalSpace X] [self : CompactSpace X] :
                                                                    IsCompact Set.univ

                                                                    In a compact space, Set.univ is a compact set.

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

                                                                    Instances

                                                                      In a noncompact space, Set.univ is not a compact set.

                                                                      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

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

                                                                        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), nnhds x, snhds x, s n IsCompact s

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

                                                                        Instances
                                                                          theorem LocallyCompactSpace.local_compact_nhds {X : Type u_3} [TopologicalSpace X] [self : LocallyCompactSpace X] (x : X) (n : Set X) :
                                                                          n nhds xsnhds x, s n IsCompact s

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

                                                                          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 : XY} {x : X} {s : Set Y}, Continuous fs nhds (f x)Knhds 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
                                                                            theorem LocallyCompactPair.exists_mem_nhds_isCompact_mapsTo {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [self : LocallyCompactPair X Y] {f : XY} {x : X} {s : Set Y} :
                                                                            Continuous fs nhds (f x)Knhds 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.

                                                                            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