Commit 2022-01-05 14:15 802f23cf

View on Github →

feat(data/fintype/basic): set_fintype_card_eq_univ_iff (#11244) Adds companion lemma to set_fintype_card_le_univ. This PR also moves several set.to_finset lemmas earlier in the file.

Estimated changes

Modified src/data/fintype/basic.lean

modified theorem set.to_finset_empty

modified theorem set.to_finset_eq_empty_iff

modified def set_fintype

added theorem set_fintype_card_eq_univ_iff

modified theorem set_fintype_card_le_univ