Using set.maps_to, inj_on, etc on finset

Stream: general

[Eric Wieser]

We have a lot of lemmas around docs#set.maps_to, but they're all written for sets. Would it make sense to generalize these for any object that implements has_mem?

[Yury G. Kudryashov]

I think, yes

[Bryan Gin-ge Chen]

It'd be good to make the interface for set,finset, etc. more uniform. I'd love to see if @Kyle Miller's proposal here for unions could be made to work.

[Kyle Miller]

(There are still some bugs with that proposal, by the way -- for example, a bounded union for set didn't seem to work. It should be fixable.)