Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes