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

• nhds x: the filter of neighborhoods of a point in a topological space, denoted by 𝓝 x in the Topology scope. A set is called a neighborhood of x, if it includes an open set around x.

• nhdsWithin x s: the filter of neighborhoods of a point within a set, defined as 𝓝 x ⊓ 𝓟 s and denoted by 𝓝[s] x. We also introduce notation for some special sets s, see below.

• nhdsSet s: the filter of neighborhoods of a set in a topological space, denoted by 𝓝ˢ s in the Topology scope. A set t is called a neighborhood of s, if it includes an open set that includes s.

### Continuity at a point #

• ContinuousAt f x: a function f is continuous at a point x, if it tends to 𝓝 (f x) along 𝓝 x.

• ContinuousWithinAt f s x: a function f is continuous within a set s at a point x, if it tends to 𝓝 (f x) along 𝓝[s] x.

• ContinuousOn f s: a function f : X → Y is continuous on a set s, if it is continuous within s at every point of s.

### Limits #

• lim f: a limit of a filter f in a nonempty topological space. If there exists x such that f ≤ 𝓝 x, then lim f is one of such points, otherwise it is Classical.choice _.

In a Hausdorff topological space, the limit is unique if it exists.

• Ultrafilter.lim f: a limit of an ultrafilter f, defined as the limit of (f : Filter X) with a proof of Nonempty X deduced from existence of an ultrafilter on X.

• limUnder f g: a limit of a filter f along a function g, defined as lim (Filter.map g f).

### Cluster points and accumulation points #

• ClusterPt x F: a point x is a cluster point of a filter F, if 𝓝 x is not disjoint with F.

• MapClusterPt x F u: a point x is a cluster point of a function u along a filter F, if it is a cluster point of the filter Filter.map u F.

• AccPt x F: a point x is an accumulation point of a filter F, if 𝓝[≠] x is not disjoint with F. Every accumulation point of a filter is its cluster point, but not vice versa.

• IsCompact s: 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. Equivalently, a set s is compact if for any cover of s by open sets, there exists a finite subcover.

• CompactSpace, NoncompactSpace: typeclasses saying that the whole space is a compact set / is not a compact set, respectively.

• WeaklyLocallyCompactSpace X: typeclass saying that every point of X has a compact neighborhood.

• LocallyCompactSpace X: typeclass saying that every point of X has a basis of compact neighborhoods. Every locally compact space is a weakly locally compact space. The reverse implication is true for R₁ (preregular) spaces.

• LocallyCompactPair X Y: an auxiliary typeclass saying that for any continuous function f : X → Y, a point x, and a neighborhood s of f x, there exists a compact neighborhood K of x such that f maps K to s.

• Filter.cocompact, Filter.coclosedCompact: filters generated by complements to compact and closed compact sets, respectively.

## Notations #

• 𝓝 x: the filter nhds x of neighborhoods of a point x;
• 𝓟 s: the principal filter of a set s, defined elsewhere;
• 𝓝[s] x: the filter nhdsWithin x s of neighborhoods of a point x within a set s;
• 𝓝[≤] x: the filter nhdsWithin x (Set.Iic x) of left-neighborhoods of x;
• 𝓝[≥] x: the filter nhdsWithin x (Set.Ici x) of right-neighborhoods of x;
• 𝓝[<] x: the filter nhdsWithin x (Set.Iio x) of punctured left-neighborhoods of x;
• 𝓝[>] x: the filter nhdsWithin x (Set.Ioi x) of punctured right-neighborhoods of x;
• 𝓝[≠] x: the filter nhdsWithin x {x}ᶜ of punctured neighborhoods of x;
• 𝓝ˢ s: the filter nhdsSet s of neighborhoods of a set.
@[irreducible]
def nhds {X : Type u_3} [] (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} [] (x : X) :
nhds x = s{s : Set X | x 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} [] (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} [] (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} [] [] (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} [] [] (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} [] [] (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
• = xs,
Instances For
def Specializes {X : Type u_1} [] (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} [] (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
def specializationPreorder (X : Type u_1) [] :

Specialization forms a preorder on the topological space.

Equations
Instances For
def inseparableSetoid (X : Type u_1) [] :

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

Equations
Instances For
def SeparationQuotient (X : Type u_1) [] :
Type u_1

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} [] [] (f : ) :
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} [] (F : ) :
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} [] {α : Type u_3} [] (f : ) (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} [] (x : X) (F : ) :

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} [] {ι : Type u_3} (x : X) (F : ) (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} [] (x : X) (F : ) :

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} [] (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
• = ∀ ⦃f : ⦄ [inst_1 : f.NeBot], xs,
Instances For
class CompactSpace (X : Type u_1) [] :

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

• isCompact_univ : IsCompact Set.univ

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

Instances
theorem CompactSpace.isCompact_univ {X : Type u_1} [] [self : ] :
IsCompact Set.univ

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

class NoncompactSpace (X : Type u_1) [] :

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

• noncompact_univ : ¬IsCompact Set.univ

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

Instances
theorem NoncompactSpace.noncompact_univ {X : Type u_1} [] [self : ] :
¬IsCompact Set.univ

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

class WeaklyLocallyCompactSpace (X : Type u_3) [] :

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), s nhds x

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

Instances
theorem WeaklyLocallyCompactSpace.exists_compact_mem_nhds {X : Type u_3} [] [self : ] (x : X) :
∃ (s : Set X), s nhds x

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

class LocallyCompactSpace (X : Type u_3) [] :

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

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} [] [self : ] (x : X) (n : Set X) :
n nhds xsnhds x, s n

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

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

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}, s nhds (f x)Knhds x, 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} [] [] [self : ] {f : XY} {x : X} {s : Set Y} :
s nhds (f x)Knhds x, 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.

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

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

Equations
• = ⨅ (s : Set X), ⨅ (_ : ),
Instances For
def Filter.coclosedCompact (X : Type u_1) [] :

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

Equations
• = ⨅ (s : Set X), ⨅ (_ : ), ⨅ (_ : ),
Instances For