Ultrafilters #
An ultrafilter is a minimal (maximal in the set order) proper filter. In this file we define
Ultrafilter.of
: an ultrafilter that is less than or equal to a given filter;Ultrafilter
: subtype of ultrafilters;pure x : Ultrafilter α
:pure x
as anUltrafilter
;Ultrafilter.map
,Ultrafilter.bind
,Ultrafilter.comap
: operations on ultrafilters;hyperfilter
: the ultrafilter extending the cofinite filter.
- univ_sets : Set.univ ∈ s.sets
- neBot' : Filter.NeBot ↑s
An ultrafilter is nontrivial.
- le_of_le : ∀ (g : Filter α), Filter.NeBot g → g ≤ ↑s → ↑s ≤ g
If
g
is a nontrivial filter that is less than or equal to an ultrafilter, then it is greater than or equal to the ultrafilter.
An ultrafilter is a minimal (maximal in the set order) proper filter.
Instances For
Alias of the forward direction of Ultrafilter.frequently_iff_eventually
.
If sᶜ ∉ f ↔ s ∈ f
, then f
is an ultrafilter. The other implication is given by
Ultrafilter.compl_not_mem_iff
.
Instances For
If f : Filter α
is an atom, then it is an ultrafilter.
Instances For
Pushforward for ultrafilters.
Instances For
The pullback of an ultrafilter along an injection whose range is large with respect to the given ultrafilter.
Instances For
The principal ultrafilter associated to a point x
.
Monadic bind for ultrafilters, coming from the one on filters defined in terms of map and join.
Instances For
The ultrafilter lemma: Any proper filter is contained in an ultrafilter.
Alias of Ultrafilter.exists_le
.
The ultrafilter lemma: Any proper filter is contained in an ultrafilter.
Construct an ultrafilter extending a given filter. The ultrafilter lemma is the assertion that such a filter exists; we use the axiom of choice to pick one.
Instances For
A filter equals the intersection of all the ultrafilters which contain it.
The tendsto
relation can be checked on ultrafilters.
The ultrafilter extending the cofinite filter.
Instances For
Alias of Filter.nmem_hyperfilter_of_finite
.
Alias of Filter.compl_mem_hyperfilter_of_finite
.
Ultrafilter extending the inf of a comapped ultrafilter and a principal ultrafilter.