Theory of filters on sets #
Main definitions #
filter
: filters on a set;at_top
,at_bot
,cofinite
,principal
: specific filters;map
,comap
: operations on filters;tendsto
: limit with respect to filters;eventually
:f.eventually p
means{x | p x} ∈ f
;frequently
:f.frequently p
means{x | ¬p x} ∉ f
;filter_upwards [h₁, ..., hₙ]
: takes a list of proofshᵢ : sᵢ ∈ f
, and replaces a goals ∈ f
with∀ x, x ∈ s₁ → ... → x ∈ sₙ → x ∈ s
;ne_bot f
: an utility class stating thatf
is a non-trivial filter.
Filters on a type X
are sets of sets of X
satisfying three conditions. 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...
In this file, we define the type filter X
of filters on X
, and endow 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:
(at_top : 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 in topology.uniform_space.basic)μ.ae
: made of sets whose complement has zero measure with respect toμ
(defined inmeasure_theory.measure_space
)
The general notion of limit of a map with respect to filters on the source and target types
is filter.tendsto
. It is defined in terms of the order and the push-forward operation.
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).
For instance, anticipating on topology.basic, the statement: "if a sequence u
converges to
some x
and u n
belongs to a set M
for n
large enough then x
is in the closure of
M
" is formalized as: tendsto u at_top (𝓝 x) → (∀ᶠ n in at_top, u n ∈ M) → x ∈ closure M
,
which is a special case of mem_closure_of_tendsto
from topology.basic.
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
: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
[ne_bot f]
in a number of lemmas and definitions.
- sets : set (set α)
- univ_sets : set.univ ∈ self.sets
- sets_of_superset : ∀ {x y : set α}, x ∈ self.sets → x ⊆ y → y ∈ self.sets
- inter_sets : ∀ {x y : set α}, x ∈ self.sets → y ∈ self.sets → x ∩ y ∈ self.sets
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 α
.
Instances for filter
- filter.has_sizeof_inst
- filter.has_mem
- filter.inhabited
- filter.partial_order
- filter.has_inf
- filter.has_top
- filter.complete_lattice
- filter.unique
- filter.distrib_lattice
- filter.order.coframe
- filter.has_pure
- filter.has_bind
- filter.has_seq
- filter.functor
- filter.applicative
- filter.alternative
- filter.can_lift
- filter.is_lawful_functor
- filter.is_lawful_applicative
- filter.is_comm_applicative
- ultrafilter.filter.has_coe_t
- filter.has_inv
- filter.has_neg
- filter.covariant_mul
- filter.covariant_add
- filter.covariant_swap_mul
- filter.covariant_swap_add
- filter.covariant_div
- filter.covariant_sub
- filter.covariant_swap_div
- filter.covariant_swap_sub
- filter.covariant_smul
- filter.covariant_vadd
- filter.covariant_smul_filter
- filter.covariant_vadd_filter
- filter.smul_comm_class_filter
- filter.vadd_comm_class_filter
- filter.smul_comm_class_filter'
- filter.vadd_comm_class_filter'
- filter.smul_comm_class_filter''
- filter.vadd_comm_class_filter''
- filter.smul_comm_class
- filter.vadd_comm_class
- filter.is_scalar_tower
- filter.vadd_assoc_class
- filter.is_scalar_tower'
- filter.vadd_assoc_class'
- filter.is_scalar_tower''
- filter.vadd_assoc_class''
- filter.is_central_scalar
An extensionality lemma that is useful for filters with good lemmas about sᶜ ∈ f
(e.g.,
filter.comap
, filter.coprod
, filter.Coprod
, filter.cofinite
).
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
.
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 filter.principal
- filter.is_countably_generated_principal
- filter.ord_connected.tendsto_Icc
- filter.tendsto_Ico_Ici_Ici
- filter.tendsto_Ico_Ioi_Ioi
- filter.tendsto_Ico_Iic_Iio
- filter.tendsto_Ico_Iio_Iio
- filter.tendsto_Ioc_Ici_Ioi
- filter.tendsto_Ioc_Iic_Iic
- filter.tendsto_Ioc_Iio_Iio
- filter.tendsto_Ioc_Ioi_Ioi
- filter.tendsto_Ioo_Ici_Ioi
- filter.tendsto_Ioo_Iic_Iio
- filter.tendsto_Ioo_Ioi_Ioi
- filter.tendsto_Ioo_Iio_Iio
- filter.tendsto_Icc_Icc_Icc
- filter.tendsto_Ioc_Icc_Icc
- filter.tendsto_Icc_interval_interval
- filter.tendsto_Ioc_interval_interval
- countable_Inter_filter_principal
Equations
- basic : ∀ {α : Type u} {g : set (set α)} {s : set α}, s ∈ g → filter.generate_sets g s
- univ : ∀ {α : Type u} {g : set (set α)}, filter.generate_sets g set.univ
- superset : ∀ {α : Type u} {g : set (set α)} {s t : set α}, filter.generate_sets g s → s ⊆ t → filter.generate_sets g t
- inter : ∀ {α : Type u} {g : set (set α)} {s t : set α}, filter.generate_sets g s → filter.generate_sets g t → filter.generate_sets g (s ∩ t)
generate_sets g s
: s
is in the filter closure of g
.
generate g
is the largest filter containing the sets g
.
Equations
- filter.generate g = {sets := filter.generate_sets g, univ_sets := _, sets_of_superset := _, inter_sets := _}
mk_of_closure 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.mk_of_closure s hs = {sets := s, univ_sets := _, sets_of_superset := _, inter_sets := _}
Galois insertion from sets of sets into filters.
Equations
- filter.gi_generate α = {choice := λ (s : set (set α)) (hs : (filter.generate s).sets ≤ s), filter.mk_of_closure s _, gc := _, le_l_u := _, choice_eq := _}
The infimum of filters is the filter generated by intersections of elements of the two filters.
Equations
- filter.has_top = {top := {sets := {s : set α | ∀ (x : α), x ∈ s}, univ_sets := _, sets_of_superset := _, inter_sets := _}}
Equations
- filter.complete_lattice = original_complete_lattice.copy partial_order.le filter.complete_lattice._proof_1 ⊤ filter.complete_lattice._proof_2 complete_lattice.bot filter.complete_lattice._proof_3 complete_lattice.sup filter.complete_lattice._proof_4 has_inf.inf filter.complete_lattice._proof_5 (filter.join ∘ filter.principal) filter.complete_lattice._proof_6 complete_lattice.Inf filter.complete_lattice._proof_7
A filter is ne_bot
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 complete_lattice
structure on filter, so
we use a typeclass argument in lemmas instead.
Instances of this typeclass
- measure_theory.is_probability_measure.ae_ne_bot
- alexandroff.nhds_within_compl_ne_bot
- filter.comap_fst_ne_bot
- filter.comap_snd_ne_bot
- filter.comap_eval_ne_bot
- filter.map_ne_bot
- filter.pure_ne_bot
- filter.prod_ne_bot'
- filter.coprod_ne_bot_left
- filter.coprod_ne_bot_right
- filter.at_top_ne_bot
- filter.at_bot_ne_bot
- filter.small_sets_ne_bot
- filter.pi_inf_principal_pi.ne_bot
- filter.pi.ne_bot
- filter.Coprod_ne_bot
- filter.cofinite_ne_bot
- ultrafilter.ne_bot
- nhds_ne_bot
- filter.cocompact.filter.ne_bot
- filter.coclosed_compact.filter.ne_bot
- nhds_within_Ici_self_ne_bot
- nhds_within_Iic_self_ne_bot
- nhds_within_Ioi_self_ne_bot
- nhds_within_Iio_self_ne_bot
- nhds_within.filter.ne_bot
- uniformity.ne_bot
- ennreal.nhds_within_Ioi_coe_ne_bot
- ennreal.nhds_within_Ioi_zero_ne_bot
- normed_field.punctured_nhds_ne_bot
- normed_field.nhds_within_is_unit_ne_bot
- real.punctured_nhds_module_ne_bot
- box_integral.integration_params.to_filter_distortion_Union_ne_bot'
- box_integral.integration_params.to_filter_distortion_ne_bot
- box_integral.integration_params.to_filter_ne_bot
- box_integral.integration_params.to_filter_Union_ne_bot
- vitali_family.filter_at_ne_bot
- alexandroff.nhds_within_compl_coe_ne_bot
- alexandroff.nhds_within_compl_infty_ne_bot
- rat.cocompact_inf_nhds_ne_bot
Lattice equations #
There is exactly one filter on an empty type. -
Equations
- filter.unique = {to_inhabited := {default := ⊥}, uniq := _}
There are only two filters on a subsingleton
: ⊥
and ⊤
. If the type is empty, then they are
equal.
Equations
- filter.distrib_lattice = {sup := complete_lattice.sup filter.complete_lattice, le := complete_lattice.le filter.complete_lattice, lt := complete_lattice.lt filter.complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf filter.complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}
Equations
- filter.order.coframe = {sup := complete_lattice.sup filter.complete_lattice, le := complete_lattice.le filter.complete_lattice, lt := complete_lattice.lt filter.complete_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf filter.complete_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, Sup := complete_lattice.Sup filter.complete_lattice, le_Sup := _, Sup_le := _, Inf := has_Inf.Inf (conditionally_complete_lattice.to_has_Inf (filter α)), Inf_le := _, le_Inf := _, top := complete_lattice.top filter.complete_lattice, bot := complete_lattice.bot filter.complete_lattice, le_top := _, bot_le := _, infi_sup_le_sup_Inf := _}
If f : ι → filter α
is directed, ι
is not empty, and ∀ i, f i ≠ ⊥
, then infi f ≠ ⊥
.
See also infi_ne_bot_of_directed
for a version assuming nonempty α
instead of nonempty ι
.
If f : ι → filter α
is directed, α
is not empty, and ∀ i, f i ≠ ⊥
, then infi f ≠ ⊥
.
See also infi_ne_bot_of_directed'
for a version assuming nonempty ι
instead of nonempty α
.
principal
equations #
Eventually #
f.eventually p
or ∀ᶠ x in f, p x
mean that {x | p x} ∈ f
. E.g., ∀ᶠ x in at_top, p x
means that p
holds true for sufficiently large x
.
Equations
- filter.eventually p f = ({x : α | p x} ∈ f)
Alias of filter.eventually_all_finite
.
Alias of filter.eventually_all_finset
.
Frequently #
f.frequently p
or ∃ᶠ x in f, p x
mean that {x | ¬p x} ∉ f
. E.g., ∃ᶠ x in at_top, p x
means that there exist arbitrarily large x
for which p
holds true.
Equations
- filter.frequently p f = ¬∀ᶠ (x : α) in f, ¬p x
Relation “eventually equal” #
Alias of the reverse direction of filter.eventually_eq_set
.
Alias of the forward direction of filter.eventually_eq_set
.
Push-forwards, pull-backs, and the monad structure #
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.map
If functions m₁
and m₂
are eventually equal at a filter f
, then
they map this filter to the same filter.
The inverse map of a filter. A set s
belongs to filter.comap f l
if either of the following
equivalent conditions hold.
- There exists a set
t ∈ l
such thatf ⁻¹' t ⊆ s
. This is used as a definition. - The set
{y | ∀ x, f x = y → x ∈ s}
belongs tol
, seefilter.mem_comap'
. - The set
(f '' sᶜ)ᶜ
belongs tol
, seefilter.mem_comap_iff_compl
andfilter.compl_mem_comap
.
Equations
- filter.comap m f = {sets := {s : set α | ∃ (t : set β) (H : t ∈ f), m ⁻¹' t ⊆ s}, univ_sets := _, sets_of_superset := _, inter_sets := _}
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
The applicative sequentiation operation. This is not induced by the bind operation.
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.has_pure = {pure := λ (α : Type u) (x : α), {sets := {s : set α | x ∈ s}, univ_sets := trivial, sets_of_superset := _, inter_sets := _}}
Equations
Equations
Equations
- filter.functor = {map := filter.map, map_const := λ (α β : Type u_1), filter.map ∘ function.const β}
The monad structure on filters.
Equations
Equations
Equations
- filter.alternative = {to_applicative := {to_functor := {map := λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : filter _x), has_pure.pure x <*> y, map_const := λ (α β : Type u_1), (λ (x : β → α) (y : filter β), has_pure.pure x <*> y) ∘ function.const β}, to_has_pure := filter.has_pure, to_has_seq := filter.has_seq, to_has_seq_left := {seq_left := λ (α β : Type u_1) (a : filter α) (b : filter β), (λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : filter _x), has_pure.pure x <*> y) α (β → α) (function.const β) a <*> b}, to_has_seq_right := {seq_right := λ (α β : Type u_1) (a : filter α) (b : filter β), (λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : filter _x), has_pure.pure x <*> y) α (β → β) (function.const α id) a <*> b}}, to_has_orelse := {orelse := λ (α : Type u_1) (x y : filter α), x ⊔ y}, failure := λ (α : Type u_1), ⊥}
map
and comap
equations #
The variables in the following lemmas are used as in this diagram:
φ
α → β
θ ↓ ↓ ψ
γ → δ
ρ
Equations
- filter.can_lift = {coe := filter.map can_lift.coe, cond := λ (f : filter α), ∀ᶠ (x : α) in f, can_lift.cond β x, prf := _}
A useful lemma when dealing with uniformities.
bind
equations #
Limits #
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₂)