Commit 2022-01-22 13:06 b630b8cd
View on Github →feat(order/antichain): Strong antichains (#11400)
This introduces a predicate is_strong_antichain
to state that a set is a strong antichain with respect to a relation.
s
is a strong (upward) antichain wrt r
if for all a ≠ b
in s
there is some c
such that ¬ r a c
or ¬ r b c
. A strong downward antichain of the swapped relation.