mathlib3

0c26bb09 - feat(data/finset/basic): add lemmas about bUnion and images of functions on finsets (#5887)

feat(data/finset/basic): add lemmas about bUnion and images of functions on finsets (#5887) Add lemmas about bUnion and images of functions on finsets. Part of #5695 in order to prove Hall's marriage theorem. Coauthors: @kmill @b-mehta Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com>