Theorem Finset.sdiff_nonempty_of_card_lt_card

Modification history

2025-03-21 12:44
Mathlib/Data/Finset/Card.lean
feat(Data/Finset/Card): add `exists_mem_not_mem_of_card_lt_card` (#23172) …
Added Finset.sdiff_nonempty_of_card_lt_cardView on Github →