Up-sets and down-sets #
This file defines upper and lower sets in an order.
Main declarations #
IsUpperSet: Predicate for a set to be an upper set. This means every element greater than a member of the set is in the set itself.
IsLowerSet: Predicate for a set to be a lower set. This means every element less than a member of the set is in the set itself.
UpperSet: The type of upper sets.
LowerSet: The type of lower sets.
upperClosure: The greatest upper set containing a set.
lowerClosure: The least lower set containing a set.
UpperSet.Ici: Principal upper set.
Set.Icias an upper set.
UpperSet.Ioi: Strict principal upper set.
Set.Ioias an upper set.
LowerSet.Iic: Principal lower set.
Set.Iicas a lower set.
LowerSet.Iio: Strict principal lower set.
Set.Iioas a lower set.
Upper sets are ordered by reverse inclusion. This convention is motivated by the fact that this
makes them order-isomorphic to lower sets and antichains, and matches the convention on
Lattice structure on antichains. Order equivalence between upper/lower sets and antichains.