Filters with countable intersection property #
In this file we define CountableInterFilter
to be the class of filters with the following
property: for any countable collection of sets s ∈ l∈ l
their intersection belongs to l
as well.
Two main examples are the residual
filter defined in Mathlib.Topology.MetricSpace.Baire
and
the measure.ae
filter defined in measure_theory.measure_space
.
We reformulate the definition in terms of indexed intersection and in terms of filter.eventually
and provide instances for some basic constructions (⊥⊥
, ⊤⊤
, Filter.principal
, Filter.map
,
Filter.comap
, Inf.inf
). We also provide a custom constructor Filter.ofCountableInter
that deduces two axioms of a Filter
from the countable intersection property.
Tags #
filter, countable
For a countable collection of sets
s ∈ l∈ l
, their intersection belongs tol
as well.
A filter l
has the countable intersection property if for any countable collection
of sets s ∈ l∈ l
their intersection belongs to l
as well.
Instances
Construct a filter with countable intersection property. This constructor deduces
Filter.univ_sets
and Filter.inter_sets
from the countable intersection property.
Equations
- One or more equations did not get rendered due to their size.
Infimum of two countable_Inter_filter
s is a countable_Inter_filter
. This is useful, e.g.,
to automatically get an instance for residual α ⊓ 𝓟 s⊓ 𝓟 s
.
Supremum of two countable_Inter_filter
s is a countable_Inter_filter
.