An ultrafilter is a minimal (maximal in the set order) proper filter. In this file we define
is_ultrafilter: a predicate stating that a given filter is an ultrafiler;
ultrafilter_of: an ultrafilter that is less than or equal to a given filter;
ultrafilter: subtype of ultrafilters;
pure xas an
ultrafilter.bind: operations on ultrafilters;
hyperfilter: the ultra-filter extending the cofinite filter.
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.