2023-12-19 17:29
Mathlib/Data/Finset/Card.lean
feat(Data/Finset/Card): the number of element satisfying `P` is no greater than `n` iff every subset with more than `n` elements contains an element not satisfying `P` (#9048)
Added Finset.card_filter_le_iff