Commit 2021-01-13 16:08 d351cfe0

feat(data/finset): sup_eq_bind (#5717) finset.sup s f is equal to finset.bind s f when f : α → finset β is an indexed family of finite sets. This is a proof of that with a couple supporting lemmas. (There might be a more direct proof through the definitions of sup and bind, which are eventually in terms of multiset.foldr.) I also moved finset.mem_sup to multiset.mem_sup and gave a new finset.mem_sup for indexed families of finset, where the old one was for indexed families of multiset.