Order filters #
Main definitions #
Throughout this file,
P is at least a preorder, but some sections
require more structure, such as a bottom element, a top element, or
a join-semilattice structure.
Order.PFilter P: The type of nonempty, downward directed, upward closed subsets of
P. This is dual to
Order.Ideal, so it simply wraps
Order.IsPFilter P: a predicate for when a
Set Pis a filter.
Note the relation between
Order/PFilter: for any
Filter α represents the same mathematical object as
PFilter (Set α).
pfilter, filter, ideal, dual