Mathlib v3 is deprecated. Go to Mathlib v4

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

Estimated changes