Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-02 04:14 0c26bb09

View on Github →

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

Estimated changes