doc-next-gen

Mathlib.Topology.Defs.Filter

Module docstring

{"# 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.

  • exterior s: 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.

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. "}
nhds definition
Full source 
/-- 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`. -/
irreducible_def nhds (x : X) : Filter X :=
  β¨… s ∈ { s : Set X | x ∈ s ∧ IsOpen s }, π“Ÿ s
Neighborhood filter of a point
Informal description
The neighborhood filter of a point $x$ in a topological space is the filter consisting of all sets that contain an open set containing $x$. Formally, it is defined as the infimum of the principal filters of all open sets containing $x$.
nhds_def theorem
: eta_helper Eq✝ @nhds.{} @(delta% @definition✝)
Full source 
/-- 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`. -/
irreducible_def nhds (x : X) : Filter X :=
  β¨… s ∈ { s : Set X | x ∈ s ∧ IsOpen s }, π“Ÿ s
Definition of Neighborhood Filter as Infimum of Open Neighborhoods
Informal description
The neighborhood filter $\mathcal{N}(x)$ of a point $x$ in a topological space is equal to the infimum of the principal filters of all open sets containing $x$, i.e., \[ \mathcal{N}(x) = \bigsqcap \{ \mathcal{P}(U) \mid U \text{ is open and } x \in U \} \] where $\mathcal{P}(U)$ denotes the principal filter generated by the set $U$.
Topology.term𝓝 definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc]
scoped[Topology] notation "𝓝" => nhds
Notation for neighborhood filter
Informal description
The notation `𝓝` is introduced as a shorthand for the neighborhood filter `nhds` in the context of topology. Specifically, for a point `x` in a topological space, `𝓝 x` represents the filter of all neighborhoods of `x`.
nhdsWithin definition
(x : X) (s : Set X) : Filter X
Full source 
/-- The "neighborhood within" filter. Elements of `𝓝[s] x` are sets containing the
intersection of `s` and a neighborhood of `x`. -/
def nhdsWithin (x : X) (s : Set X) : Filter X :=
  𝓝𝓝 x βŠ“ π“Ÿ s
Neighborhood filter within a set
Informal description
The neighborhood filter within a set $s$ at a point $x$ in a topological space, denoted $\mathcal{N}_s(x)$, is the filter consisting of all subsets that contain the intersection of $s$ with some neighborhood of $x$. Formally, it is defined as the infimum of the neighborhood filter $\mathcal{N}(x)$ and the principal filter generated by $s$.
Topology.term𝓝[_]_ definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc]
scoped[Topology] notation "𝓝[" s "] " x:100 => nhdsWithin x s
Notation for neighborhood filter within a set
Informal description
The notation `𝓝[s] x` represents the filter of neighborhoods of a point `x` within a set `s` in a topological space, which is defined as the infimum of the neighborhood filter `𝓝 x` and the principal filter of `s`.
Topology.nhdsNE definition
: Lean.ParserDescr✝
Full source 
/-- Notation for the filter of punctured neighborhoods of a point. -/
scoped[Topology] notation3 (name := nhdsNE) "𝓝[β‰ ] " x:100 =>
  nhdsWithin x (@singleton _ (Set _) Set.instSingletonSet x)ᢜ
Punctured neighborhood filter notation
Informal description
The notation `𝓝[β‰ ] x` represents the filter of punctured neighborhoods of a point `x`, which consists of all sets that contain an open neighborhood of `x` excluding `x` itself. Formally, it is defined as the neighborhood filter of `x` within the complement of the singleton set `{x}`.
Topology.nhdsNE.delab_app.nhdsWithin definition
: Delab✝
Full source 
/-- Notation for the filter of punctured neighborhoods of a point. -/
scoped[Topology] notation3 (name := nhdsNE) "𝓝[β‰ ] " x:100 =>
  nhdsWithin x (@singleton _ (Set _) Set.instSingletonSet x)ᢜ
Punctured neighborhoods filter notation
Informal description
The notation `𝓝[β‰ ] x` represents the filter of punctured neighborhoods of a point `x` in a topological space, defined as the neighborhoods of `x` excluding `x` itself. More precisely, it is the filter `nhdsWithin x {x}ᢜ`, where `{x}ᢜ` denotes the complement of the singleton set containing `x`.
Topology.nhdsGE definition
: Lean.ParserDescr✝
Full source 
/-- Notation for the filter of right neighborhoods of a point. -/
scoped[Topology] notation3 (name := nhdsGE) "𝓝[β‰₯] " x:100 => nhdsWithin x (Set.Ici x)
Right neighborhoods filter notation
Informal description
The notation `𝓝[β‰₯] x` represents the filter of right neighborhoods of a point `x` in a topological space, defined as the neighborhoods of `x` within the closed interval `[x, ∞)`. More precisely, it is the filter `nhdsWithin x (Set.Ici x)`, where `Set.Ici x` denotes the set of all points greater than or equal to `x`.
Topology.nhdsGE.delab_app.nhdsWithin definition
: Delab✝
Full source 
/-- Notation for the filter of right neighborhoods of a point. -/
scoped[Topology] notation3 (name := nhdsGE) "𝓝[β‰₯] " x:100 => nhdsWithin x (Set.Ici x)
Right-neighborhood filter notation
Informal description
The notation `𝓝[β‰₯] x` represents the filter of right-neighborhoods of a point `x` in a topological space, defined as the neighborhood filter of `x` restricted to the closed interval `[x, ∞)` (the set of all points greater than or equal to `x`).
Topology.nhdsLE definition
: Lean.ParserDescr✝
Full source 
/-- Notation for the filter of left neighborhoods of a point. -/
scoped[Topology] notation3 (name := nhdsLE) "𝓝[≀] " x:100 => nhdsWithin x (Set.Iic x)
Left neighborhood filter
Informal description
The notation `𝓝[≀] x` denotes the filter of left neighborhoods of a point `x`, which consists of all sets containing an open interval extending to the left of `x`. Formally, it is defined as the neighborhood filter of `x` restricted to the set `(-∞, x]`.
Topology.nhdsGT.delab_app.nhdsWithin definition
: Delab✝
Full source 
/-- Notation for the filter of punctured right neighborhoods of a point. -/
scoped[Topology] notation3 (name := nhdsGT) "𝓝[>] " x:100 => nhdsWithin x (Set.Ioi x)
Notation for punctured right neighborhoods filter
Informal description
The notation `𝓝[>] x` represents the filter of punctured right neighborhoods of a point `x` in a topological space, defined as the neighborhood filter of `x` restricted to the open interval `(x, ∞)`.
Topology.nhdsLT definition
: Lean.ParserDescr✝
Full source 
/-- Notation for the filter of punctured left neighborhoods of a point. -/
scoped[Topology] notation3 (name := nhdsLT) "𝓝[<] " x:100 => nhdsWithin x (Set.Iio x)
Punctured left neighborhoods filter
Informal description
The notation `𝓝[<] x` represents the filter of punctured left neighborhoods of a point `x` in a topological space, which consists of all sets containing an open interval to the left of `x` but not including `x` itself.
nhdsSet definition
(s : Set X) : Filter X
Full source 
/-- The filter of neighborhoods of a set in a topological space. -/
def nhdsSet (s : Set X) : Filter X :=
  sSup (nhdsnhds '' s)
Neighborhood filter of a set
Informal description
The neighborhood filter of a set $s$ in a topological space is the supremum of the neighborhood filters of all points in $s$. A set $t$ is a neighborhood of $s$ if it contains an open set that includes $s$.
Topology.term𝓝˒ definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc] scoped[Topology] notation "𝓝˒" => nhdsSet
Neighborhood filter of a set
Informal description
The notation `𝓝˒ s` represents the filter of neighborhoods of a set `s` in a topological space, where `s` is a subset of the space. A set `t` is called a neighborhood of `s` if it includes an open set that contains `s`.
exterior definition
(s : Set X) : Set X
Full source 
/-- 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`. -/
def exterior (s : Set X) : Set X := (𝓝˒ s).ker
Exterior of a set
Informal description
The *exterior* of a set $s$ in a topological space is the intersection of all neighborhoods of $s$. In an Alexandrov-discrete space, this coincides with the smallest neighborhood of $s$.
ContinuousAt definition
(f : X β†’ Y) (x : X)
Full source 
/-- A function between topological spaces is continuous at a point `xβ‚€`
if `f x` tends to `f xβ‚€` when `x` tends to `xβ‚€`. -/
@[fun_prop]
def ContinuousAt (f : X β†’ Y) (x : X) :=
  Tendsto f (𝓝 x) (𝓝 (f x))
Continuity at a point
Informal description
A function $f \colon X \to Y$ between topological spaces is continuous at a point $x_0 \in X$ if for every neighborhood $V$ of $f(x_0)$ in $Y$, there exists a neighborhood $U$ of $x_0$ in $X$ such that $f(U) \subseteq V$. Equivalently, $f$ tends to $f(x_0)$ along the neighborhood filter of $x_0$.
ContinuousWithinAt definition
(f : X β†’ Y) (s : Set X) (x : X) : Prop
Full source 
/-- 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`. -/
@[fun_prop]
def ContinuousWithinAt (f : X β†’ Y) (s : Set X) (x : X) : Prop :=
  Tendsto f (𝓝[s] x) (𝓝 (f x))
Continuity within a subset at a point
Informal description
A function \( f \colon X \to Y \) between topological spaces is continuous at a point \( x_0 \) within a subset \( s \subseteq X \) if, for every neighborhood \( V \) of \( f(x_0) \) in \( Y \), there exists a neighborhood \( U \) of \( x_0 \) in \( X \) such that \( f(U \cap s) \subseteq V \). Equivalently, \( f \) tends to \( f(x_0) \) along the filter of neighborhoods of \( x_0 \) within \( s \).
ContinuousOn definition
(f : X β†’ Y) (s : Set X) : Prop
Full source 
/-- A function between topological spaces is continuous on a subset `s`
when it's continuous at every point of `s` within `s`. -/
@[fun_prop]
def ContinuousOn (f : X β†’ Y) (s : Set X) : Prop :=
  βˆ€ x ∈ s, ContinuousWithinAt f s x
Continuity on a subset
Informal description
A function \( f \colon X \to Y \) between topological spaces is continuous on a subset \( s \subseteq X \) if it is continuous at every point \( x \in s \) within \( s \). That is, for every \( x \in s \), the function \( f \) tends to \( f(x) \) along the filter of neighborhoods of \( x \) within \( s \).
Specializes definition
(x y : X) : Prop
Full source 
/-- `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`. -/
def Specializes (x y : X) : Prop := 𝓝 x ≀ 𝓝 y
Specialization relation between points in a topological space
Informal description
We say that a point $x$ *specializes* to a point $y$ in a topological space $X$ (denoted $x \rightsquigarrow y$) if any of the following equivalent conditions holds: 1. The neighborhood filter of $x$ is finer than the neighborhood filter of $y$ (i.e., $\mathcal{N}_x \leq \mathcal{N}_y$); 2. Every neighborhood of $y$ contains $x$ (i.e., $\{x\} \leq \mathcal{N}_y$); 3. $y$ belongs to the closure of $\{x\}$; 4. The closure of $\{y\}$ is contained in the closure of $\{x\}$; 5. For any closed set $s$, if $x \in s$ then $y \in s$; 6. For any open set $s$, if $y \in s$ then $x \in s$; 7. $y$ is a cluster point of the principal filter $\mathcal{P}\{x\}$. This relation defines a preorder on $X$. If $X$ is a Tβ‚€ space, the preorder becomes a partial order. If $X$ is a T₁ space, the relation reduces to equality ($x \rightsquigarrow y$ if and only if $x = y$).
term_β€³_ definition
: Lean.TrailingParserDescr✝
Full source 
@[inherit_doc]
infixl:300 " β€³ " => Specializes
Specialization relation
Informal description
The notation `x β€³ y` represents the specialization relation between points `x` and `y` in a topological space, meaning that `y` is in the closure of `{x}` (or equivalently, every neighborhood of `y` contains `x`).
Inseparable definition
(x y : X) : Prop
Full source 
/-- 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`.
-/
def Inseparable (x y : X) : Prop :=
  𝓝 x = 𝓝 y
Inseparable points in a topological space
Informal description
Two points $x$ and $y$ in a topological space are called *inseparable* if they have identical neighborhood filters, i.e., $\mathcal{N}_x = \mathcal{N}_y$. This is equivalent to: - Having the same membership in all open sets - Having the same membership in all closed sets - Each point being in the closure of the other - Having identical closures of their singletons
specializationPreorder definition
: Preorder X
Full source 
/-- Specialization forms a preorder on the topological space. -/
def specializationPreorder : Preorder X :=
  { Preorder.lift (OrderDual.toDualOrderDual.toDual ∘ 𝓝) with
    le := fun x y => y β€³ x
    lt := fun x y => y ″ xy ″ x ∧ ¬x ″ y }
Specialization preorder on a topological space
Informal description
The specialization preorder on a topological space $X$ is defined by $x \leq y$ if and only if $y$ specializes to $x$ (i.e., every neighborhood of $x$ contains $y$). This forms a preorder where: - The relation $\leq$ is reflexive and transitive. - The strict relation $<$ is defined by $x < y$ if $y \rightsquigarrow x$ but not $x \rightsquigarrow y$. Equivalently, this preorder can be obtained by lifting the dual order of the neighborhood filter inclusion via the map $x \mapsto \mathcal{N}_x$.
inseparableSetoid definition
: Setoid X
Full source 
/-- A `setoid` version of `Inseparable`, used to define the `SeparationQuotient`. -/
def inseparableSetoid : Setoid X := { Setoid.comap 𝓝 βŠ₯ with r := Inseparable }
Inseparable equivalence relation on a topological space
Informal description
The equivalence relation on a topological space `X` where two points `x` and `y` are equivalent if they are inseparable (i.e., they have identical neighborhood filters, $\mathcal{N}_x = \mathcal{N}_y$). This relation is used to define the `SeparationQuotient` of the space.
SeparationQuotient definition
Full source 
/-- The quotient of a topological space by its `inseparableSetoid`.
This quotient is guaranteed to be a Tβ‚€ space. -/
def SeparationQuotient := Quotient (inseparableSetoid X)
Separation quotient of a topological space
Informal description
The `SeparationQuotient` of a topological space $X$ is the quotient space obtained by identifying points that are inseparable (i.e., points $x$ and $y$ for which the neighborhood filters $\mathcal{N}_x$ and $\mathcal{N}_y$ coincide). This quotient space is guaranteed to be a $T_0$ space, meaning that any two distinct points have distinct neighborhood filters.
lim definition
[Nonempty X] (f : Filter X) : X
Full source 
/-- If `f` is a filter, then `Filter.lim f` is a limit of the filter, if it exists. -/
noncomputable def lim [Nonempty X] (f : Filter X) : X :=
  Classical.epsilon fun x => f ≀ 𝓝 x
Limit of a filter in a nonempty topological space
Informal description
Given a nonempty topological space `X` and a filter `f` on `X`, the limit of `f` is a point `x` in `X` such that `f` converges to `x` (i.e., `f` is finer than the neighborhood filter of `x`). If such a point exists, `lim f` returns one of them; otherwise, it returns an arbitrary point in `X` (using the axiom of choice via `Classical.epsilon`).
limUnder definition
{Ξ± : Type*} [Nonempty X] (f : Filter Ξ±) (g : Ξ± β†’ X) : X
Full source 
/-- 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. -/
noncomputable def limUnder {Ξ± : Type*} [Nonempty X] (f : Filter Ξ±) (g : Ξ± β†’ X) : X :=
  lim (f.map g)
Limit of a function along a filter
Informal description
Given a nonempty topological space \( X \), a filter \( f \) on a type \( \alpha \), and a function \( g : \alpha \to X \), the limit of \( g \) along \( f \) is defined as the limit of the image filter \( f.map \, g \) in \( X \). If there exists a point \( x \) in \( X \) such that \( f.map \, g \) converges to \( x \), then \( \text{limUnder} \, f \, g \) returns one such \( x \); otherwise, it returns an arbitrary point in \( X \).
ClusterPt definition
(x : X) (F : Filter X) : Prop
Full source 
/-- 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. -/
def ClusterPt (x : X) (F : Filter X) : Prop :=
  NeBot (𝓝𝓝 x βŠ“ F)
Cluster point of a filter
Informal description
A point $x$ in a topological space is a cluster point of a filter $F$ if the infimum of the neighborhood filter of $x$ and $F$ is not the trivial filter (i.e., $\mathcal{N}_x \sqcap F \neq \bot$). This means that every neighborhood of $x$ intersects every set in $F$ in a non-empty set. Note that this differs from being an accumulation point, which would require the punctured neighborhood filter $\mathcal{N}_{x \neq x} \sqcap F$ to be non-trivial.
MapClusterPt definition
{ΞΉ : Type*} (x : X) (F : Filter ΞΉ) (u : ΞΉ β†’ X) : Prop
Full source 
/-- 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`. -/
def MapClusterPt {ΞΉ : Type*} (x : X) (F : Filter ΞΉ) (u : ΞΉ β†’ X) : Prop :=
  ClusterPt x (map u F)
Cluster point of a function along a filter
Informal description
A point \( x \) in a topological space is a cluster point of a function \( u \) along a filter \( F \) if \( x \) is a cluster point of the filter obtained by mapping \( u \) over \( F \). In other words, \( x \) is a cluster point of \( u \) along \( F \) if the neighborhood filter of \( x \) and the image filter \( u(F) \) have a non-trivial intersection (i.e., \(\mathcal{N}_x \sqcap u(F) \neq \bot\)).
AccPt definition
(x : X) (F : Filter X) : Prop
Full source 
/-- A point `x` is an accumulation point of a filter `F` if `𝓝[β‰ ] x βŠ“ F β‰  βŠ₯`.
See also `ClusterPt`. -/
def AccPt (x : X) (F : Filter X) : Prop :=
  NeBot (𝓝[β‰ ] x𝓝[β‰ ] x βŠ“ F)
Accumulation point of a filter
Informal description
A point \( x \) in a topological space is an *accumulation point* of a filter \( F \) if the infimum of the punctured neighborhood filter of \( x \) (i.e., the filter of neighborhoods of \( x \) excluding \( x \) itself) and \( F \) is not the trivial filter. In other words, \( \mathcal{N}_{x \neq x} \sqcap F \neq \bot \), meaning every punctured neighborhood of \( x \) intersects every set in \( F \) in a non-empty set.
IsCompact definition
(s : Set X)
Full source 
/-- 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`. -/
def IsCompact (s : Set X) :=
  βˆ€ ⦃f⦄ [NeBot f], f ≀ π“Ÿ s β†’ βˆƒ x ∈ s, ClusterPt x f
Compact subset of a topological space
Informal description
A subset $s$ of a topological space $X$ is called *compact* if for every nontrivial filter $F$ that contains $s$ (i.e., $F \leq \mathcal{P} s$), there exists a point $x \in s$ such that $x$ is a cluster point of $F$. This means that every neighborhood of $x$ intersects every set in $F$ non-trivially.
CompactSpace structure
Full source 
/-- Type class for compact spaces. Separation is sometimes included in the definition, especially
in the French literature, but we do not include it here. -/
class CompactSpace : Prop where
  /-- In a compact space, `Set.univ` is a compact set. -/
  isCompact_univ : IsCompact (Set.univ : Set X)
Compact Space
Informal description
A structure representing the property of a topological space being compact, meaning every open cover has a finite subcover. This does not include any separation axioms in its definition (though some mathematical traditions, particularly French literature, may include separation in the definition of compactness).
NoncompactSpace structure
Full source 
/-- `X` is a noncompact topological space if it is not a compact space. -/
class NoncompactSpace : Prop where
  /-- In a noncompact space, `Set.univ` is not a compact set. -/
  noncompact_univ : Β¬IsCompact (Set.univ : Set X)
Noncompact topological space
Informal description
A topological space \( X \) is called a *noncompact space* if it is not a compact space, meaning there exists an open cover of \( X \) that does not admit a finite subcover.
WeaklyLocallyCompactSpace structure
(X : Type*) [TopologicalSpace X]
Full source 
/-- We say that a topological space is a *weakly locally compact space*,
if each point of this space admits a compact neighborhood. -/
class WeaklyLocallyCompactSpace (X : Type*) [TopologicalSpace X] : Prop where
  /-- Every point of a weakly locally compact space admits a compact neighborhood. -/
  exists_compact_mem_nhds (x : X) : βˆƒ s, IsCompact s ∧ s ∈ 𝓝 x
Weakly Locally Compact Space
Informal description
A topological space \( X \) is called *weakly locally compact* if every point \( x \in X \) has a compact neighborhood, i.e., there exists a compact set \( K \) containing \( x \) in its interior.
LocallyCompactSpace structure
(X : Type*) [TopologicalSpace X]
Full source 
/-- 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. -/
class LocallyCompactSpace (X : Type*) [TopologicalSpace X] : Prop where
  /-- In a locally compact space,
    every neighbourhood of every point contains a compact neighbourhood of that same point. -/
  local_compact_nhds : βˆ€ (x : X), βˆ€ n ∈ 𝓝 x, βˆƒ s ∈ 𝓝 x, s βŠ† n ∧ IsCompact s
Locally Compact Space
Informal description
A topological space \( X \) is called *locally compact* if every point \( x \in X \) has a neighborhood basis consisting of compact sets. This means that for every neighborhood \( U \) of \( x \), there exists a compact neighborhood \( K \) of \( x \) such that \( K \subseteq U \).
LocallyCompactPair structure
(X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y]
Full source 
/-- 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.
-/
class LocallyCompactPair (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y] : Prop where
  /-- 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`. -/
  exists_mem_nhds_isCompact_mapsTo : βˆ€ {f : X β†’ Y} {x : X} {s : Set Y},
    Continuous f β†’ s ∈ 𝓝 (f x) β†’ βˆƒ K ∈ 𝓝 x, IsCompact K ∧ Set.MapsTo f K s
Locally Compact Pair of Topological Spaces
Informal description
A pair of topological spaces \( X \) and \( Y \) is called a *locally compact pair* if for any continuous function \( f : X \to Y \), any point \( x \in X \), and any neighborhood \( s \) of \( f(x) \), there exists a compact neighborhood \( K \) of \( x \) such that \( f(K) \subseteq s \). This condition is satisfied in two main cases: 1. When \( X \) is a locally compact space. 2. When \( X \) is weakly locally compact and \( Y \) is an R₁ (preregular) space.
Filter.cocompact definition
: Filter X
Full source 
/-- `Filter.cocompact` is the filter generated by complements to compact sets. -/
def Filter.cocompact : Filter X :=
  β¨… (s : Set X) (_ : IsCompact s), π“Ÿ sᢜ
Filter of complements of compact sets
Informal description
The filter `Filter.cocompact` on a topological space \( X \) is defined as the infimum of all principal filters generated by the complements of compact subsets of \( X \). In other words, it consists of all subsets of \( X \) that contain the complement of some compact set.
Filter.coclosedCompact definition
: Filter X
Full source 
/-- `Filter.coclosedCompact` is the filter generated by complements to closed compact sets.
In a Hausdorff space, this is the same as `Filter.cocompact`. -/
def Filter.coclosedCompact : Filter X :=
  β¨… (s : Set X) (_ : IsClosed s) (_ : IsCompact s), π“Ÿ sᢜ
Filter of complements of closed compact sets
Informal description
The filter `Filter.coclosedCompact` on a topological space \( X \) is defined as the infimum of all principal filters generated by the complements of closed and compact subsets of \( X \). In other words, it consists of all subsets of \( X \) that contain the complement of some closed compact set. In a Hausdorff space, this filter coincides with the cocompact filter.