Commit 2021-01-25 17:49 5491c592

View on Github →

feat(data/fintype/basic): add lemmas about finsets and cardinality (#5886) Add lemmas about finsets and cardinality. Part of #5695 in order to prove Hall's marriage theorem. Coauthors: @kmill @b-mehta

Estimated changes

Modified src/data/fintype/basic.lean

added theorem finset.card_compl_lt_iff_nonempty

added theorem finset.card_eq_iff_eq_univ

added theorem finset.card_lt_iff_ne_univ

added theorem finset.compl_ne_univ_iff_nonempty