Theorem Multiset.card_filter_le_iff

Modification history

2025-02-25 17:02
Mathlib/Data/Multiset/Basic.lean
chore(Data/Multiset): split `Multiset/Basic.lean` into many files (#22126) …
Modified Multiset.card_filter_le_iffView on Github →
2023-12-19 17:29
Mathlib/Data/Multiset/Basic.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 Multiset.card_filter_le_iffView on Github →