finset.disjoint_bind

Stream: general

[Yury G. Kudryashov]

What would be a good name for a version of finset.bind (s : finset α) (t : α → finset β) that knows for sure that t x are pairwise disjoint?

[Adam Topaz]

branch?

[Kenny Lau]

don't define partial functions; prove partial theorems