Commit 2021-02-16 12:05 914517b5
View on Github →feat(order/well_founded_set): finite antidiagonal of well-founded sets (#6208)
Defines set.add_antidiagonal s t a
, the set of pairs of an element from s
and an element from t
that add to a
If s
and t
are well-founded, then constructs a finset version, finset.add_antidiagonal_of_is_wf