Theory of filters on sets #
A filter on a type α
is a collection of sets of α
which contains the whole α
,
is upwards-closed, and is stable under intersection. They are mostly used to
abstract two related kinds of ideas:
- limits, including finite or infinite limits of sequences, finite or infinite limits of functions at a point or at infinity, etc...
- things happening eventually, including things happening for large enough
n : ℕ
, or near enough a pointx
, or for close enough pairs of points, or things happening almost everywhere in the sense of measure theory. Dually, filters can also express the idea of things happening often: for arbitrarily largen
, or at a point in any neighborhood of given a point etc...
Main definitions #
In this file, we endow Filter α
it with a complete lattice structure.
This structure is lifted from the lattice structure on Set (Set X)
using the Galois
insertion which maps a filter to its elements in one direction, and an arbitrary set of sets to
the smallest filter containing it in the other direction.
We also prove Filter
is a monadic functor, with a push-forward operation
Filter.map
and a pull-back operation Filter.comap
that form a Galois connections for the
order on filters.
The examples of filters appearing in the description of the two motivating ideas are:
(Filter.atTop : Filter ℕ)
: made of sets ofℕ
containing{n | n ≥ N}
for someN
𝓝 x
: made of neighborhoods ofx
in a topological space (defined in topology.basic)𝓤 X
: made of entourages of a uniform space (those space are generalizations of metric spaces defined inMathlib/Topology/UniformSpace/Basic.lean
)MeasureTheory.ae
: made of sets whose complement has zero measure with respect toμ
(defined inMathlib/MeasureTheory/OuterMeasure/AE
)
The predicate "happening eventually" is Filter.Eventually
, and "happening often" is
Filter.Frequently
, whose definitions are immediate after Filter
is defined (but they come
rather late in this file in order to immediately relate them to the lattice structure).
Notations #
∀ᶠ x in f, p x
:f.Eventually p
;∃ᶠ x in f, p x
:f.Frequently p
;f =ᶠ[l] g
:∀ᶠ x in l, f x = g x
;f ≤ᶠ[l] g
:∀ᶠ x in l, f x ≤ g x
;𝓟 s
:Filter.Principal s
, localized inFilter
.
References #
Important note: Bourbaki requires that a filter on X
cannot contain all sets of X
, which
we do not require. This gives Filter X
better formal properties, in particular a bottom element
⊥
for its lattice structure, at the cost of including the assumption
[NeBot f]
in a number of lemmas and definitions.
An extensionality lemma that is useful for filters with good lemmas about sᶜ ∈ f
(e.g.,
Filter.comap
, Filter.coprod
, Filter.Coprod
, Filter.cofinite
).
Weaker version of Filter.iInter_mem
that assumes Subsingleton β
rather than Finite β
.
GenerateSets g s
: s
is in the filter closure of g
.
- basic {α : Type u} {g : Set (Set α)} {s : Set α} : s ∈ g → Filter.GenerateSets g s
- univ {α : Type u} {g : Set (Set α)} : Filter.GenerateSets g Set.univ
- superset {α : Type u} {g : Set (Set α)} {s t : Set α} : Filter.GenerateSets g s → s ⊆ t → Filter.GenerateSets g t
- inter {α : Type u} {g : Set (Set α)} {s t : Set α} : Filter.GenerateSets g s → Filter.GenerateSets g t → Filter.GenerateSets g (s ∩ t)
Instances For
generate g
is the largest filter containing the sets g
.
Equations
- Filter.generate g = { sets := {s : Set α | Filter.GenerateSets g s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Instances For
mkOfClosure s hs
constructs a filter on α
whose elements set is exactly
s : Set (Set α)
, provided one gives the assumption hs : (generate s).sets = s
.
Equations
- Filter.mkOfClosure s hs = { sets := s, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Instances For
Galois insertion from sets of sets into filters.
Equations
- Filter.giGenerate α = { choice := fun (s : Set (Set α)) (hs : (Filter.generate s).sets ≤ s) => Filter.mkOfClosure s ⋯, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
Complete lattice structure on Filter α
.
Equations
- Filter.instCompleteLatticeFilter = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Either f = ⊥
or Filter.NeBot f
. This is a version of eq_or_ne
that uses Filter.NeBot
as the second alternative, to be used as an instance.
Alias of the reverse direction of Filter.principal_mono
.
Lattice equations #
There are only two filters on a Subsingleton
: ⊥
and ⊤
. If the type is empty, then they are
equal.
Equations
- Filter.instDistribLattice = DistribLattice.mk ⋯
If f : ι → Filter α
is directed, ι
is not empty, and ∀ i, f i ≠ ⊥
, then iInf f ≠ ⊥
.
See also iInf_neBot_of_directed
for a version assuming Nonempty α
instead of Nonempty ι
.
If f : ι → Filter α
is directed, α
is not empty, and ∀ i, f i ≠ ⊥
, then iInf f ≠ ⊥
.
See also iInf_neBot_of_directed'
for a version assuming Nonempty ι
instead of Nonempty α
.
principal
equations #
Alias of the reverse direction of Filter.principal_neBot_iff
.
Eventually #
Alias of Filter.Eventually.of_forall
.
Frequently #
Alias of Filter.Frequently.of_forall
.
Alias of the forward direction of Filter.frequently_inf_principal
.
Alias of the reverse direction of Filter.frequently_inf_principal
.
Relation “eventually equal” #
Alias of Filter.EventuallyEq.of_eq
.
Push-forwards, pull-backs, and the monad structure #
If functions m₁
and m₂
are eventually equal at a filter f
, then
they map this filter to the same filter.
The analog of kernImage
for filters. A set s
belongs to Filter.kernMap m f
if either of
the following equivalent conditions hold.
- There exists a set
t ∈ f
such thats = kernImage m t
. This is used as a definition. - There exists a set
t
such thattᶜ ∈ f
andsᶜ = m '' t
, seeFilter.mem_kernMap_iff_compl
andFilter.compl_mem_kernMap
.
This definition because it gives a right adjoint to Filter.comap
, and because it has a nice
interpretation when working with co-
filters (Filter.cocompact
, Filter.cofinite
, ...).
For example, kernMap m (cocompact α)
is the filter generated by the complements of the sets
m '' K
where K
is a compact subset of α
.
Equations
- Filter.kernMap m f = { sets := Set.kernImage m '' f.sets, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Instances For
Filter
as a Monad
#
In this section we define Filter.monad
, a Monad
structure on Filter
s. This definition is not
an instance because its Seq
projection is not equal to the Filter.seq
function we use in the
Applicative
instance on Filter
.
The variables in the following lemmas are used as in this diagram:
φ
α → β
θ ↓ ↓ ψ
γ → δ
ρ
Temporary lemma that we can tag with gcongr
Temporary lemma that we can tag with gcongr
A useful lemma when dealing with uniformities.
bind
equations #
Alias of the reverse direction of Filter.map_surjOn_Iic_iff_surjOn
.
Alias of the reverse direction of Filter.filter_injOn_Iic_iff_injOn
.