Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-03 07:41 62c06a55

View on Github →

feat(data/finset/basic): a finset has card at most one iff it is contained in a singleton (#7404)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.card_le_one_iff

added theorem finset.card_le_one_iff_subset_singleton

added theorem finset.card_le_one_of_subsingleton

added theorem finset.one_lt_card_iff

Modified src/data/fintype/basic.lean

deleted theorem finset.card_le_one_iff

deleted theorem finset.card_le_one_of_subsingleton

deleted theorem finset.one_lt_card_iff