Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-10-30 15:07 65a1391a

View on Github →

feat(data/{list,multiset,finset}/*): attach and filter lemmas (#18087) Left commutativity and cardinality of list.filter/multiset.filter/finset.filter. Interaction of count/countp and attach.

Estimated changes

added theorem finset.card_filter
added theorem finset.prod_map_val
modified theorem finset.sum_boole
added theorem finset.card_val
added theorem finset.filter_attach'
added theorem finset.filter_attach
added theorem finset.map_filter'
added theorem list.attach_nil
added theorem list.filter_attach'
added theorem list.filter_attach
added theorem list.filter_comm
added theorem list.map_filter'
added theorem list.count_attach
added theorem list.countp_attach
added theorem multiset.count_attach
added theorem multiset.countp_attach
added theorem multiset.filter_attach
added theorem multiset.filter_comm
added theorem multiset.map_filter'
modified theorem multiset.sup_le