Definitions about filters in topological spaces #
In this file we define filters in topological spaces,
as well as other definitions that rely on Filter
s.
Main Definitions #
Neighborhoods filter #

nhds x
: the filter of neighborhoods of a point in a topological space, denoted by𝓝 x
in theTopology
scope. A set is called a neighborhood ofx
, if it includes an open set aroundx
. 
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 setss
, see below. 
nhdsSet s
: the filter of neighborhoods of a set in a topological space, denoted by𝓝ˢ s
in theTopology
scope. A sett
is called a neighborhood ofs
, if it includes an open set that includess
.
Continuity at a point #

ContinuousAt f x
: a functionf
is continuous at a pointx
, if it tends to𝓝 (f x)
along𝓝 x
. 
ContinuousWithinAt f s x
: a functionf
is continuous within a sets
at a pointx
, if it tends to𝓝 (f x)
along𝓝[s] x
. 
ContinuousOn f s
: a functionf : X → Y
is continuous on a sets
, if it is continuous withins
at every point ofs
.
Limits #

lim f
: a limit of a filterf
in a nonempty topological space. If there existsx
such thatf ≤ 𝓝 x
, thenlim f
is one of such points, otherwise it isClassical.choice _
.In a Hausdorff topological space, the limit is unique if it exists.

Ultrafilter.lim f
: a limit of an ultrafilterf
, defined as the limit of(f : Filter X)
with a proof ofNonempty X
deduced from existence of an ultrafilter onX
. 
limUnder f g
: a limit of a filterf
along a functiong
, defined aslim (Filter.map g f)
.
Cluster points and accumulation points #

ClusterPt x F
: a pointx
is a cluster point of a filterF
, if𝓝 x
is not disjoint withF
. 
MapClusterPt x F u
: a pointx
is a cluster point of a functionu
along a filterF
, if it is a cluster point of the filterFilter.map u F
. 
AccPt x F
: a pointx
is an accumulation point of a filterF
, if𝓝[≠] x
is not disjoint withF
. Every accumulation point of a filter is its cluster point, but not vice versa. 
IsCompact s
: a sets
is compact if for every nontrivial filterf
that containss
, there existsa ∈ s
such that every set off
meets every neighborhood ofa
. Equivalently, a sets
is compact if for any cover ofs
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 ofX
has a compact neighborhood. 
LocallyCompactSpace X
: typeclass saying that every point ofX
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 functionf : X → Y
, a pointx
, and a neighborhoods
off x
, there exists a compact neighborhoodK
ofx
such thatf
mapsK
tos
. 
Filter.cocompact
,Filter.coclosedCompact
: filters generated by complements to compact and closed compact sets, respectively.
Notations #
𝓝 x
: the filternhds x
of neighborhoods of a pointx
;𝓟 s
: the principal filter of a sets
, defined elsewhere;𝓝[s] x
: the filternhdsWithin x s
of neighborhoods of a pointx
within a sets
;𝓝[≤] x
: the filternhdsWithin x (Set.Iic x)
of leftneighborhoods ofx
;𝓝[≥] x
: the filternhdsWithin x (Set.Ici x)
of rightneighborhoods ofx
;𝓝[<] x
: the filternhdsWithin x (Set.Iio x)
of punctured leftneighborhoods ofx
;𝓝[>] x
: the filternhdsWithin x (Set.Ioi x)
of punctured rightneighborhoods ofx
;𝓝[≠] x
: the filternhdsWithin x {x}ᶜ
of punctured neighborhoods ofx
;𝓝ˢ s
: the filternhdsSet s
of neighborhoods of a set.
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
.
Instances For
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
 Topology.term𝓝 = Lean.ParserDescr.node `Topology.term𝓝 1024 (Lean.ParserDescr.symbol "𝓝")
Instances For
The "neighborhood within" filter. Elements of 𝓝[s] x
are sets containing the
intersection of s
and a neighborhood of x
.
Equations
 nhdsWithin x s = nhds x ⊓ Filter.principal s
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
 Topology.«term𝓝[≠]_» = Lean.ParserDescr.node `Topology.term𝓝[≠]_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓝[≠] ") (Lean.ParserDescr.cat `term 100))
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
 Topology.«term𝓝[≥]_» = Lean.ParserDescr.node `Topology.term𝓝[≥]_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓝[≥] ") (Lean.ParserDescr.cat `term 100))
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
 Topology.«term𝓝[≤]_» = Lean.ParserDescr.node `Topology.term𝓝[≤]_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓝[≤] ") (Lean.ParserDescr.cat `term 100))
Instances For
Notation for the filter of punctured right neighborhoods of a point.
Equations
 Topology.«term𝓝[>]_» = Lean.ParserDescr.node `Topology.term𝓝[>]_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓝[>] ") (Lean.ParserDescr.cat `term 100))
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
 Topology.«term𝓝[<]_» = Lean.ParserDescr.node `Topology.term𝓝[<]_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓝[<] ") (Lean.ParserDescr.cat `term 100))
Instances For
Pretty printer defined by notation3
command.
Equations
 One or more equations did not get rendered due to their size.
Instances For
The filter of neighborhoods of a set in a topological space.
Equations
 Topology.«term𝓝ˢ» = Lean.ParserDescr.node `Topology.term𝓝ˢ 1024 (Lean.ParserDescr.symbol "𝓝ˢ")
Instances For
A function between topological spaces is continuous at a point x₀
if f x
tends to f x₀
when x
tends to x₀
.
Equations
 ContinuousAt f x = Filter.Tendsto f (nhds x) (nhds (f x))
Instances For
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
 ContinuousWithinAt f s x = Filter.Tendsto f (nhdsWithin x s) (nhds (f x))
Instances For
A function between topological spaces is continuous on a subset s
when it's continuous at every point of s
within s
.
Equations
 ContinuousOn f s = ∀ x ∈ s, ContinuousWithinAt f s x
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 ofy
containsx
;y ∈ closure {x}
;closure {y} ⊆ closure {x}
; for any closed set
s
we havex ∈ s → y ∈ s
;  for any open set
s
we havey ∈ s → x ∈ s
; y
is a cluster point of the filterpure 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
.
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 ofy
containsx
;y ∈ closure {x}
;closure {y} ⊆ closure {x}
; for any closed set
s
we havex ∈ s → y ∈ s
;  for any open set
s
we havey ∈ s → x ∈ s
; y
is a cluster point of the filterpure 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
 «term_⤳_» = Lean.ParserDescr.trailingNode `term_⤳_ 300 300 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⤳ ") (Lean.ParserDescr.cat `term 301))
Instances For
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
, seeinseparable_iff_open
;  for any closed set
s
,x ∈ s ↔ y ∈ s
, seeinseparable_iff_closed
; x ∈ closure {y}
andy ∈ closure {x}
, seeinseparable_iff_mem_closure
;closure {x} = closure {y}
, seeinseparable_iff_closure_eq
.
Equations
 Inseparable x y = (nhds x = nhds y)
Instances For
Specialization forms a preorder on the topological space.
Equations
 specializationPreorder X = let __src := Preorder.lift (⇑OrderDual.toDual ∘ nhds); Preorder.mk ⋯ ⋯ ⋯
Instances For
A setoid
version of Inseparable
, used to define the SeparationQuotient
.
Equations
 inseparableSetoid X = let __src := Setoid.comap nhds ⊥; { r := Inseparable, iseqv := ⋯ }
Instances For
The quotient of a topological space by its inseparableSetoid
.
This quotient is guaranteed to be a T₀ space.
Equations
Instances For
If f
is a filter, then Filter.lim f
is a limit of the filter, if it exists.
Equations
 lim f = Classical.epsilon fun (x : X) => f ≤ nhds x
Instances For
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
 Ultrafilter.lim F = lim ↑F
Instances For
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
 ClusterPt x F = Filter.NeBot (nhds x ⊓ F)
Instances For
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
 MapClusterPt x F u = ClusterPt x (Filter.map u F)
Instances For
A point x
is an accumulation point of a filter F
if 𝓝[≠] x ⊓ F ≠ ⊥
.
See also ClusterPt
.
Equations
 AccPt x F = Filter.NeBot (nhdsWithin x {x}ᶜ ⊓ F)
Instances For
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
 IsCompact s = ∀ ⦃f : Filter X⦄ [inst_1 : Filter.NeBot f], f ≤ Filter.principal s → ∃ x ∈ s, ClusterPt x f
Instances For
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.
In a noncompact space,
Set.univ
is not a compact set.
Instances
We say that a topological space is a weakly locally compact space, if each point of this space admits a compact neighborhood.
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 compactopen topology.
See also WeaklyLocallyCompactSpace
, a typeclass that only assumes
that each point has a compact neighborhood.
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 andY
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 ands : Set Y
is a neighbourhood off x
,x : X
, then there exists a compact neighbourhoodK
ofx
such thatf
mapsK
tos
.
Instances
Filter.cocompact
is the filter generated by complements to compact sets.
Equations
 Filter.cocompact X = ⨅ (s : Set X), ⨅ (_ : IsCompact s), Filter.principal sᶜ
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
 Filter.coclosedCompact X = ⨅ (s : Set X), ⨅ (_ : IsClosed s), ⨅ (_ : IsCompact s), Filter.principal sᶜ