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 ofP
. This is dual toOrder.Ideal
, so it simply wrapsOrder.Ideal Pᵒᵈ
.Order.IsPFilter P
: a predicate for when aSet P
is a filter.
Note the relation between Order/Filter
and Order/PFilter
: for any
type α
, Filter α
represents the same mathematical object as
PFilter (Set α)
.
References #
Tags #
pfilter, filter, ideal, dual
- dual : Order.Ideal Pᵒᵈ
A filter on a preorder P
is a subset of P
that is
- nonempty
- downward directed
- upward closed.
Instances For
Create an element of type Order.PFilter
from a set satisfying the predicate
Order.IsPFilter
.
Instances For
A filter on P
is a subset of P
.
Two filters are equal when their underlying sets are equal.
The smallest filter containing a given element.
Instances For
A specific witness of pfilter.nonempty
when P
has a top element.
There is a bottom filter when P
has a top element.
There is a top filter when P
has a bottom element.
A specific witness of pfilter.directed
when P
has meets.
If a poset P
admits arbitrary Inf
s, then principal
and Inf
form a Galois coinsertion.