mathlib3
6b475a41 - feat(data/finset/basic): `finset.two_lt_card` (#11505)

Commit
3 years ago
feat(data/finset/basic): `finset.two_lt_card` (#11505) This PR adds lemmas `finset.two_lt_card` and `finset.two_lt_card_iff`, similar to `finset.one_lt_card` and `finset.one_lt_card_iff`. These lemmas are also similar to `finset.card_eq_three`.
Author
Parents
Loading