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 (order_dual P)
.order.is_pfilter 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 (order_dual P)
A filter on a preorder P
is a subset of P
that is
- nonempty
- downward directed
- upward closed.
A predicate for when a subset of P
is a filter.
Equations
Create an element of type order.pfilter
from a set satisfying the predicate
order.is_pfilter
.
Equations
- h.to_pfilter = {dual := order.is_ideal.to_ideal h}
A filter on P
is a subset of P
.
Equations
- order.pfilter.set.has_coe = {coe := λ (F : order.pfilter P), F.dual.carrier}
For the notation x ∈ F
.
Equations
- order.pfilter.has_mem = {mem := λ (x : P) (F : order.pfilter P), x ∈ ↑F}
The smallest filter containing a given element.
Equations
Equations
Two filters are equal when their underlying sets are equal.
The partial ordering by subset inclusion, inherited from set P
.
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.