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 xas an
ultrafilter.comap: operations on ultrafilters;
hyperfilter: the ultrafilter extending the cofinite filter.
sᶜ ∉ f ↔ s ∈ f, then
f is an ultrafilter. The other implication is given by
The pullback of an ultrafilter along an injection whose range is large with respect to the given ultrafilter.