Commit 2020-07-17 12:38 207a1d4e
View on Github →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.
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.