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;
An ultrafilter is a minimal (maximal in the set order) proper filter.
- neBot' : (↑self).NeBot
An ultrafilter is nontrivial.
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.
Instances For
Equations
Alias of Ultrafilter.compl_notMem_iff
.
Alias of the forward direction of Ultrafilter.frequently_iff_eventually
.
Alias of Ultrafilter.compl_mem_iff_notMem
.
If sᶜ ∉ f ↔ s ∈ f
, then f
is an ultrafilter. The other implication is given by
Ultrafilter.compl_notMem_iff
.
Equations
Instances For
Alias of Ultrafilter.empty_notMem
.
Pushforward for ultrafilters.
Equations
Instances For
The pullback of an ultrafilter along an injection whose range is large with respect to the given ultrafilter.
Equations
Instances For
The principal ultrafilter associated to a point x
.
Equations
Equations
Monadic bind for ultrafilters, coming from the one on filters defined in terms of map and join.
Equations
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.
Equations
Instances For
A filter equals the intersection of all the ultrafilters which contain it.
Ultrafilter extending the inf of a comapped ultrafilter and a principal ultrafilter.