Definitions about filters #
A filter on a type α
is a collection of sets of α
which contains the whole α
,
is upwards-closed, and is stable under intersection. Filters 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 #
Filter
: filters on a set;Filter.principal
,𝓟 s
: filter of all sets containing a given set;Filter.map
,Filter.comap
: operations on filters;Filter.Tendsto
: limit with respect to filters;Filter.Eventually
:f.Eventually p
means{x | p x} ∈ f
;Filter.Frequently
:f.Frequently p
means{x | ¬p x} ∉ f
;filter_upwards [h₁, ..., hₙ]
: a tactic that takes a list of proofshᵢ : sᵢ ∈ f
, and replaces a goals ∈ f
with∀ x, x ∈ s₁ → ... → x ∈ sₙ → x ∈ s
;Filter.NeBot f
: a utility class stating thatf
is a non-trivial filter.Filter.IsBounded r f
: the filterf
is eventually bounded w.r.t. the relationr
, i.e. eventually, it is bounded by some uniform bound.r
will be usually instantiated with(· ≤ ·)
or(· ≥ ·)
.Filter.IsCobounded r f
states that the filterf
does not tend to infinity w.r.t.r
. This is also called frequently bounded. Will be usually instantiated with(· ≤ ·)
or(· ≥ ·)
.
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
.
Implementation Notes #
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.
References #
- [N. Bourbaki, General Topology][bourbaki1966]
A filter F
on a type α
is a collection of sets of α
which contains the whole α
,
is upwards-closed, and is stable under intersection. We do not forbid this collection to be
all sets of α
.
The set of sets that belong to the filter.
The set
Set.univ
belongs to any filter.If a set belongs to a filter, then its superset belongs to the filter as well.
If two sets belong to a filter, then their intersection belongs to the filter as well.
Instances For
If F
is a filter on α
, and U
a subset of α
then we can write U ∈ F
as on paper.
Equations
Construct a filter from a property that is stable under finite unions.
A set s
belongs to Filter.comk p _ _ _
iff its complement satisfies the predicate p
.
This constructor is useful to define filters like Filter.cofinite
.
Equations
Instances For
The principal filter of s
is the collection of all supersets of s
.
Equations
Instances For
The principal filter of s
is the collection of all supersets of s
.
Equations
Instances For
pure x
is the set of sets that contain x
. It is equal to 𝓟 {x}
but
with this definition we have s ∈ pure a
defeq a ∈ s
.
Equations
The kernel of a filter is the intersection of all its sets.
Equations
Instances For
The infimum of filters is the filter generated by intersections of elements of the two filters.
Equations
The supremum of two filters is the filter that contains sets that belong to both filters.
Equations
A filter is NeBot
if it is not equal to ⊥
, or equivalently the empty set does not belong to
the filter. Bourbaki include this assumption in the definition of a filter but we prefer to have a
CompleteLattice
structure on Filter _
, so we use a typeclass argument in lemmas instead.
The filter is nontrivial:
f ≠ ⊥
or equivalently,∅ ∉ f
.
Instances
f.Eventually p
or ∀ᶠ x in f, p x
mean that {x | p x} ∈ f
. E.g., ∀ᶠ x in atTop, p x
means that p
holds true for sufficiently large x
.
Equations
Instances For
f.Eventually p
or ∀ᶠ x in f, p x
mean that {x | p x} ∈ f
. E.g., ∀ᶠ x in atTop, p x
means that p
holds true for sufficiently large x
.
Equations
Instances For
Pretty printer defined by notation3
command.
Equations
Instances For
f.Frequently p
or ∃ᶠ x in f, p x
mean that {x | ¬p x} ∉ f
. E.g., ∃ᶠ x in atTop, p x
means that there exist arbitrarily large x
for which p
holds true.
Equations
Instances For
f.Frequently p
or ∃ᶠ x in f, p x
mean that {x | ¬p x} ∉ f
. E.g., ∃ᶠ x in atTop, p x
means that there exist arbitrarily large x
for which p
holds true.
Equations
Instances For
Pretty printer defined by notation3
command.
Equations
Instances For
Two functions f
and g
are eventually equal along a filter l
if the set of x
such that
f x = g x
belongs to l
.
Equations
Instances For
A function f
is eventually less than or equal to a function g
at a filter l
.
Equations
Instances For
Filter.Tendsto
is the generic "limit of a function" predicate.
Tendsto f l₁ l₂
asserts that for every l₂
neighborhood a
,
the f
-preimage of a
is an l₁
neighborhood.
Equations
Instances For
The inverse map of a filter. A set s
belongs to Filter.comap m f
if either of the following
equivalent conditions hold.
- There exists a set
t ∈ f
such thatm ⁻¹' t ⊆ s
. This is used as a definition. - The set
kernImage m s = {y | ∀ x, m x = y → x ∈ s}
belongs tof
, seeFilter.mem_comap'
. - The set
(m '' sᶜ)ᶜ
belongs tof
, seeFilter.mem_comap_iff_compl
andFilter.compl_mem_comap
.
Equations
Instances For
Product of filters. This is the filter generated by cartesian products
of elements of the component filters.
Deprecated. Use f ×ˢ g
instead.
Equations
Instances For
The monadic bind operation on filter is defined the usual way in terms of map
and join
.
Unfortunately, this bind
does not result in the expected applicative. See Filter.seq
for the
applicative instance.
Equations
Instances For
f.IsBoundedUnder (≺) u
: the image of the filter f
under u
is eventually bounded w.r.t.
the relation ≺
, i.e. eventually, it is bounded by some uniform bound.
Equations
Instances For
IsCobounded (≺) f
states that the filter f
does not tend to infinity w.r.t. ≺
. This is
also called frequently bounded. Will be usually instantiated with ≤
or ≥
.
There is a subtlety in this definition: we want f.IsCobounded
to hold for any f
in the case of
complete lattices. This will be relevant to deduce theorems on complete lattices from their
versions on conditionally complete lattices with additional assumptions. We have to be careful in
the edge case of the trivial filter containing the empty set: the other natural definition
¬ ∀ a, ∀ᶠ n in f, a ≤ n
would not work as well in this case.
Equations
Instances For
IsCoboundedUnder (≺) f u
states that the image of the filter f
under the map u
does not
tend to infinity w.r.t. ≺
. This is also called frequently bounded. Will be usually instantiated
with ≤
or ≥
.
Equations
Instances For
filter_upwards [h₁, ⋯, hₙ]
replaces a goal of the form s ∈ f
and terms
h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f
with ∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s
.
The list is an optional parameter, []
being its default value.
filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ
is a short form for
{ filter_upwards [h₁, ⋯, hₙ], intros a₁ a₂ ⋯ aₖ }
.
filter_upwards [h₁, ⋯, hₙ] using e
is a short form for
{ filter_upwards [h1, ⋯, hn], exact e }
.
Combining both shortcuts is done by writing filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e
.
Note that in this case, the aᵢ
terms can be used in e
.