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.Ici
as an upper set.UpperSet.Ioi
: Strict principal upper set.Set.Ioi
as an upper set.LowerSet.Iic
: Principal lower set.Set.Iic
as a lower set.LowerSet.Iio
: Strict principal lower set.Set.Iio
as a lower set.
Notation #
×ˢ
is notation forUpperSet.prod
/LowerSet.prod
.
Notes #
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 Filter
.
TODO #
Lattice structure on antichains. Order equivalence between upper/lower sets and antichains.
Unbundled upper/lower sets #
Alias of the reverse direction of isLowerSet_preimage_ofDual_iff
.
Alias of the reverse direction of isUpperSet_preimage_ofDual_iff
.
Alias of the reverse direction of isLowerSet_preimage_toDual_iff
.
Alias of the reverse direction of isUpperSet_preimage_toDual_iff
.
Alias of the forward direction of isUpperSet_iff_Ici_subset
.
Alias of the forward direction of isLowerSet_iff_Iic_subset
.
Alias of the forward direction of isUpperSet_iff_Ioi_subset
.
Alias of the forward direction of isLowerSet_iff_Iio_subset
.
Bundled upper/lower sets #
Order #
Complement #
Map #
Principal sets #
The smallest upper set containing a given element.
Instances For
The smallest upper set containing a given element.
Instances For
upperClosure
forms a reversed Galois insertion with the coercion from upper sets to sets.
Instances For
lowerClosure
forms a Galois insertion with the coercion from lower sets to sets.
Instances For
Alias of the forward direction of bddAbove_lowerClosure
.
Alias of the reverse direction of bddAbove_lowerClosure
.
Alias of the reverse direction of bddBelow_upperClosure
.
Alias of the forward direction of bddBelow_upperClosure
.