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

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

.

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

- «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`

, 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

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

.

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

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

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

In a compact space, `Set.univ`

is a compact set.

`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

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.

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.

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

## Instances

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

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

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