f.is_bounded (≺): the filter f is eventually bounded w.r.t. the relation ≺, i.e. eventually, it is bounded by some uniform bound. r will be usually instantiated with ≤ or ≥.

f is eventually bounded if and only if, there exists an admissible set on which it is bounded.

A bounded function u is in particular eventually bounded.

is_cobounded (≺) f states that filter f is not tend to infinite w.r.t. ≺. This is also called frequently bounded. Will be usually instantiated with ≤ or ≥.

There is a subtlety in this definition: we want f.is_cobounded to hold for any f in the case of complete lattices. This will be relevant to deduce theorems on complete lattices from their versions on conditionally complete lattices with additional assumptions. We have to be careful in the edge case of the trivial filter containing the empty set: the other natural definition ¬ ∀a, {n | a ≤ n} ∈ f.sets would not work as well in this case.

To check that a filter is frequently bounded, it suffices to have a witness which bounds f at some point for every admissible set.

This is only an implication, as the other direction is wrong for the trivial filter.

A filter which is eventually bounded is in particular frequently bounded (in the opposite direction). At least if the filter is not trivial.

In a complete lattice, the limsup of a function is the infimum over sets s in the filter of the supremum of the function over s

In a complete lattice, the liminf of a function is the infimum over sets s in the filter of the supremum of the function over s