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 #

source
theorem nhds_def {X : Type u_3} [TopologicalSpace X] (x : X) :
nhds x = ⨅ s ∈ {s : Set X | x ∈ s ∧ IsOpen s}, Filter.principal s
source
@[irreducible]
def nhds {X : Type u_3} [TopologicalSpace X] (x : X) :
Filter 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
source
def Topology.term𝓝 :
Lean.ParserDescr

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
source
def nhdsWithin {X : Type u_1} [TopologicalSpace X] (x : X) (s : Set X) :
Filter X

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

Equations
source
def Topology.«term𝓝[_]_» :
Lean.ParserDescr

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.
source
def Topology.«term𝓝[≠]_» :
Lean.ParserDescr

Notation for the filter of punctured neighborhoods of a point.

Equations
source
def Topology.«term𝓝[≠]_».delab :
Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations
  • One or more equations did not get rendered due to their size.
source
def Topology.«term𝓝[≥]_».delab :
Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations
  • One or more equations did not get rendered due to their size.
source
def Topology.«term𝓝[≥]_» :
Lean.ParserDescr

Notation for the filter of right neighborhoods of a point.

Equations
source
def Topology.«term𝓝[≤]_» :
Lean.ParserDescr

Notation for the filter of left neighborhoods of a point.

Equations
source
def Topology.«term𝓝[≤]_».delab :
Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations
  • One or more equations did not get rendered due to their size.
source
def Topology.«term𝓝[>]_».delab :
Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations
  • One or more equations did not get rendered due to their size.
source
def Topology.«term𝓝[>]_» :
Lean.ParserDescr

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

Equations
source
def Topology.«term𝓝[<]_» :
Lean.ParserDescr

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

Equations
source
def Topology.«term𝓝[<]_».delab :
Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations
  • One or more equations did not get rendered due to their size.
source
def nhdsSet {X : Type u_1} [TopologicalSpace X] (s : Set X) :
Filter X

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

Equations
source
def Topology.«term𝓝ˢ» :
Lean.ParserDescr

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

Equations
source
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
source
def ContinuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (x : X) :
Prop

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

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

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
source
def ContinuousOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (s : Set X) :
Prop

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

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

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
source
def «term_⤳_» :
Lean.TrailingParserDescr

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
source
def Inseparable {X : Type u_1} [TopologicalSpace X] (x : X) (y : X) :
Prop

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
source
def specializationPreorder (X : Type u_1) [TopologicalSpace X] :
Preorder X

Specialization forms a preorder on the topological space.

Equations
source
def inseparableSetoid (X : Type u_1) [TopologicalSpace X] :
Setoid X

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

Equations
source
def SeparationQuotient (X : Type u_1) [TopologicalSpace X] :
Type u_1

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

Equations
source
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
source
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
source
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
source
def ClusterPt {X : Type u_1} [TopologicalSpace X] (x : X) (F : Filter X) :
Prop

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
source
def MapClusterPt {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} (x : X) (F : Filter ι) (u : ι → X) :
Prop

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
source
def AccPt {X : Type u_1} [TopologicalSpace X] (x : X) (F : Filter X) :
Prop

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

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

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
source
class CompactSpace (X : Type u_1) [TopologicalSpace X] :
Prop

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

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

    source
    class NoncompactSpace (X : Type u_1) [TopologicalSpace X] :
    Prop

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

    Instances
      source
      theorem NoncompactSpace.noncompact_univ {X : Type u_1} :
      ∀ {inst : TopologicalSpace X} [self : NoncompactSpace X], ¬IsCompact Set.univ

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

      source
      class WeaklyLocallyCompactSpace (X : Type u_3) [TopologicalSpace X] :
      Prop

      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
        source
        theorem WeaklyLocallyCompactSpace.exists_compact_mem_nhds {X : Type u_3} :
        ∀ {inst : TopologicalSpace X} [self : WeaklyLocallyCompactSpace X] (x : X), ∃ (s : Set X), IsCompact s ∧ s ∈ nhds x

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

        source
        class LocallyCompactSpace (X : Type u_3) [TopologicalSpace X] :
        Prop

        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 ∈ 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
          source
          theorem LocallyCompactSpace.local_compact_nhds {X : Type u_3} :
          ∀ {inst : TopologicalSpace X} [self : LocallyCompactSpace X] (x : 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.

          source
          class LocallyCompactPair (X : Type u_3) (Y : Type u_4) [TopologicalSpace X] [TopologicalSpace Y] :
          Prop

          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
            source
            theorem LocallyCompactPair.exists_mem_nhds_isCompact_mapsTo {X : Type u_3} {Y : Type u_4} :
            ∀ {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y} [self : LocallyCompactPair X Y] {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.

            source
            def Filter.cocompact (X : Type u_1) [TopologicalSpace X] :
            Filter X

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

            Equations
            source
            def Filter.coclosedCompact (X : Type u_1) [TopologicalSpace X] :
            Filter X

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

            Equations