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.
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.
- univ_sets : Set.univ ∈ self.sets
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.
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
- Filter.comk p he hmono hunion = { sets := {t : Set α | p tᶜ}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Instances For
The principal filter of s
is the collection of all supersets of s
.
Equations
- Filter.principal s = { sets := {t : Set α | s ⊆ t}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Instances For
The principal filter of s
is the collection of all supersets of s
.
Equations
- Filter.term𝓟 = Lean.ParserDescr.node `Filter.term𝓟 1024 (Lean.ParserDescr.symbol "𝓟")
Instances For
Equations
- Filter.instPartialOrder = PartialOrder.mk ⋯
The infimum of filters is the filter generated by intersections of elements of the two filters.
The supremum of two filters is the filter that contains sets that belong to both filters.
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
- Filter.Eventually p f = ({x : α | p x} ∈ f)
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
- 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
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
- Filter.Frequently p f = ¬∀ᶠ (x : α) in f, ¬p x
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
- 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
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
- One or more equations did not get rendered due to their size.
Instances For
A function f
is eventually less than or equal to a function g
at a filter l
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward map of a filter
Equations
- Filter.map m f = { sets := Set.preimage m ⁻¹' f.sets, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
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
- Filter.Tendsto f l₁ l₂ = (Filter.map f l₁ ≤ l₂)
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
- Filter.comap m f = { sets := {s : Set α | ∃ t ∈ f, m ⁻¹' t ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }
Instances For
Product of filters. This is the filter generated by cartesian products of elements of the component filters.
Equations
- f.prod g = Filter.comap Prod.fst f ⊓ Filter.comap Prod.snd g
Instances For
Coproduct of filters.
Equations
- f.coprod g = Filter.comap Prod.fst f ⊔ Filter.comap Prod.snd g
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
- f.bind m = (Filter.map m f).join
Instances For
The applicative sequentiation operation. This is not induced by the bind operation.
Equations
Instances For
This filter is characterized by Filter.eventually_curry_iff
:
(∀ᶠ (x : α × β) in f.curry g, p x) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y)
. Useful
in adding quantifiers to the middle of Tendsto
s. See
hasFDerivAt_of_tendstoUniformlyOnFilter
.
Equations
- f.curry g = f.bind fun (a : α) => Filter.map (fun (x : β) => (a, x)) g
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
- Filter.instFunctor = { map := @Filter.map, mapConst := fun {α β : Type ?u.8} => Filter.map ∘ Function.const β }
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
.
Equations
- One or more equations did not get rendered due to their size.