mathlib3

914517b5 - feat(order/well_founded_set): finite antidiagonal of well-founded sets (#6208)

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`