If F is a filter on α, and U a subset of α then we can write U ∈ F as on paper.
filter_upwards [h1, ⋯, hn] replaces a goal of the form s ∈ f and terms h1 : t1 ∈ f, ⋯, hn : tn ∈ f with ∀x, x ∈ t1 → ⋯ → x ∈ tn → x ∈ s.
filter_upwards [h1, ⋯, hn] e is a short form for { filter_upwards [h1, ⋯, hn], exact e }.
The principal filter of s is the collection of all supersets of s.
The join of a filter of filters is defined by the relation s ∈ join f ↔ {t | s ∈ t} ∈ f.
generate_sets g s: s is in the filter closure of g.
generate g is the smallest filter containing the sets g.
The infimum of filters is the filter generated by intersections of elements of the two filters.
The forward map of a filter
The inverse map of a filter
The cofinite filter is the filter of subsets whose complements are finite.
The monadic bind operation on filter is defined the usual way in terms of map and join.
Unfortunately, this bind does not result in the expected applicative. See filter.seq for the applicative instance.
The applicative sequentiation operation. This is not induced by the bind operation.
tendsto is the generic "limit of a function" predicate. tendsto f l₁ l₂ asserts that for every l₂ neighborhood a, the f-preimage of a is an l₁ neighborhood.
Product of filters. This is the filter generated by cartesian products of elements of the component filters.
at_top is the filter representing the limit → ∞ on an ordered set. It is generated by the collection of up-sets {b | a ≤ b}. (The preorder need not have a top element for this to be well defined, and indeed is trivial when a top element exists.)
at_bot is the filter representing the limit → -∞ on an ordered set. It is generated by the collection of down-sets {b | b ≤ a}. (The preorder need not have a bottom element for this to be well defined, and indeed is trivial when a bottom element exists.)
A function f grows to infinity independent of an order-preserving embedding e.
A function f maps upwards closed sets (at_top sets) to upwards closed sets when it is a Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an insertion and a connetion above b'.
An ultrafilter is a minimal (maximal in the set order) proper filter.
Equivalent characterization of ultrafilters: A filter f is an ultrafilter if and only if for each set s, -s belongs to f if and only if s does not belong to f.
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.
A filter equals the intersection of all the ultrafilters which contain it.
The tendsto relation can be checked on ultrafilters.