finset.bUnion vs finset.sup

Stream: general

[Yaël Dillies]

We have docs#finset.bUnion although this is a special case of docs#finset.sup. Should we unify both?
For context, we don't have finset.bInter, but we do have finset.inf.

[Kyle Miller]

In particular, docs#finset.sup_eq_bUnion relates them. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/finsets.2C.20unions.2C.20and.20cardinality/near/222486579

There's a mild difference between them if it matters: docs#finset.bUnion uses the underlying docs#multiset.bind in its implementation, so the way it works computationally is it concatenates all the lists then removes duplicates; many lemmas about finset.bUnion are lifted from their multiset counterparts. docs#finset.sup on the other hand, when specialized to finset.bUnion, iteratively computes pairwise unions, so it removes duplicates as it goes; everything needs to be reproved in terms of properties of docs#finset.fold.

docs#finset.sup_def seems relatively unused, so maybe it makes sense pushing as much as possible down into lemmas about docs#multiset.sup

If there's a finset.bInter, it likely wouldn't go by that name, though I suspect people usually write something using docs#finset.filter (one issue: a finset.bInter needs at least one finset in the intersection if you don't have a fintype constraint).