Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-19 05:53 8067812e

View on Github →

feat(data/multiset): filter, count, distrib lattice

Estimated changes

Modified data/list/basic.lean

deleted theorem list.count_cons_ge_count

added theorem list.count_le_count_cons

modified theorem list.count_pos

deleted theorem list.count_pos_of_mem

added theorem list.countp_pos

deleted theorem list.countp_pos_of_mem

added theorem list.diff_append

added theorem list.eq_of_sublist_of_length_le

deleted theorem list.exists_mem_of_countp_pos

added theorem list.length_pos_iff_exists_mem

modified theorem list.map_const

deleted theorem list.mem_of_count_pos

Modified data/list/perm.lean

Modified data/multiset/basic.lean

added theorem multiset.add_inter_distrib

added theorem multiset.add_union_distrib

modified theorem multiset.card_add

added theorem multiset.card_pos_iff_exists_mem

added theorem multiset.card_repeat

added theorem multiset.card_sub

added theorem multiset.coe_count

added theorem multiset.coe_countp

added theorem multiset.coe_filter

added def multiset.count

added theorem multiset.count_add

added theorem multiset.count_cons_of_ne

added theorem multiset.count_cons_self

added theorem multiset.count_eq_zero

added theorem multiset.count_eq_zero_of_not_mem

added theorem multiset.count_erase_of_ne

added theorem multiset.count_erase_self

added theorem multiset.count_inter

added theorem multiset.count_le_count_cons

added theorem multiset.count_le_of_le

added theorem multiset.count_pos

added theorem multiset.count_repeat

added theorem multiset.count_singleton

added theorem multiset.count_sub

added theorem multiset.count_union

added theorem multiset.count_zero

added def multiset.countp

added theorem multiset.countp_add

added theorem multiset.countp_cons_of_neg

added theorem multiset.countp_cons_of_pos

added theorem multiset.countp_eq_card_filter

added theorem multiset.countp_le_of_le

added theorem multiset.countp_pos

added theorem multiset.countp_pos_of_mem

added theorem multiset.countp_sub

added theorem multiset.countp_zero

deleted theorem multiset.empty_subset

deleted theorem multiset.eq_empty_of_forall_not_mem

deleted theorem multiset.eq_empty_of_subset_empty

modified theorem multiset.eq_of_le_of_card_le

added theorem multiset.eq_of_mem_map_const

added theorem multiset.eq_of_mem_repeat

added theorem multiset.eq_repeat'

added theorem multiset.eq_repeat

added theorem multiset.eq_repeat_of_mem

added theorem multiset.eq_zero_of_forall_not_mem

modified theorem multiset.eq_zero_of_le_zero

added theorem multiset.eq_zero_of_subset_zero

deleted theorem multiset.exists_mem_of_ne_empty

added theorem multiset.exists_mem_of_ne_zero

added theorem multiset.ext

added def multiset.filter

added theorem multiset.filter_add

added theorem multiset.filter_cons_of_neg

added theorem multiset.filter_cons_of_pos

added theorem multiset.filter_eq_nil

added theorem multiset.filter_eq_self

added theorem multiset.filter_inter

added theorem multiset.filter_le

added theorem multiset.filter_le_filter

added theorem multiset.filter_sub

modified theorem multiset.filter_subset

modified theorem multiset.filter_union

added theorem multiset.filter_zero

added theorem multiset.inf_eq_inter

added theorem multiset.inter_add_distrib

added theorem multiset.le_count_iff_repeat_le

added theorem multiset.le_filter

added theorem multiset.le_iff_count

added theorem multiset.map_const

modified theorem multiset.mem_filter

added theorem multiset.mem_filter_of_mem

added theorem multiset.mem_of_mem_filter

deleted theorem multiset.not_mem_empty

added theorem multiset.not_mem_zero

added theorem multiset.of_mem_filter

added def multiset.repeat

added theorem multiset.repeat_le_coe

added theorem multiset.repeat_subset_singleton

modified theorem multiset.singleton_coe

added theorem multiset.sub_add'

added theorem multiset.sub_add_inter

added theorem multiset.sub_inter

deleted theorem multiset.subset_empty_iff

added theorem multiset.subset_zero_iff

added theorem multiset.sup_eq_union

added theorem multiset.union_add_distrib

added theorem multiset.union_add_inter

added theorem multiset.zero_subset

Modified data/nat/basic.lean

added theorem nat.pred_sub

added theorem nat.sub_add_eq_max

added theorem nat.sub_add_min

added theorem nat.sub_min