mathlib3

207a1d4e - feat(data/finset/basic): finset of empty type (#3425)

feat(data/finset/basic): finset of empty type (#3425) In a proof working by cases for whether a type is nonempty, I found I had a use for the result that a `finset` of an empty type is empty.