Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-24 05:19 e5764291

View on Github →

feat(data/multiset): filter_map

Estimated changes

Modified data/multiset/basic.lean

added theorem multiset.coe_filter_map

added theorem multiset.filter_filter_map

added def multiset.filter_map

added theorem multiset.filter_map_cons_none

added theorem multiset.filter_map_cons_some

added theorem multiset.filter_map_eq_filter

added theorem multiset.filter_map_eq_map

added theorem multiset.filter_map_filter

added theorem multiset.filter_map_filter_map

added theorem multiset.filter_map_le_filter_map

added theorem multiset.filter_map_map

added theorem multiset.filter_map_some

added theorem multiset.filter_map_zero

added theorem multiset.map_filter_map

added theorem multiset.map_filter_map_of_inv

added theorem multiset.mem_filter_map

added theorem multiset.nodup_filter_map