Commit 2025-01-06 12:46 88c4a940

View on Github →

chore(Data/Multiset/Basic): move the sub, union, inter sections lower (#19863)

  • Move the sections about sub, union and inter under the sections about count and filter
  • Multiset.countP_sub now has a different argument order to match List.countP_diff
  • Golf List.count_sub
  • Name the instances and declare them using where notation
  • Define Multiset.card using Quotient.lift, not Quotient.liftOn

Estimated changes

modified theorem Multiset.add_inter_distrib
modified theorem Multiset.add_union_distrib
modified def Multiset.card
modified theorem Multiset.card_sub
modified theorem Multiset.coe_inter
modified theorem Multiset.coe_sub
modified theorem Multiset.cons_inter_distrib
modified theorem Multiset.cons_inter_of_neg
modified theorem Multiset.cons_inter_of_pos
modified theorem Multiset.cons_sub_of_le
modified theorem Multiset.cons_union_distrib
modified theorem Multiset.countP_sub
modified theorem Multiset.count_inter
modified theorem Multiset.count_sub
modified theorem Multiset.count_union
modified theorem Multiset.eq_union_left
modified theorem Multiset.eq_union_right
modified theorem Multiset.erase_attach_map
modified theorem Multiset.filter_inter
modified theorem Multiset.filter_sub
modified theorem Multiset.filter_union
modified theorem Multiset.inf_eq_inter
modified theorem Multiset.inter_add_distrib
modified theorem Multiset.inter_comm
modified theorem Multiset.inter_le_left
modified theorem Multiset.inter_le_right
modified theorem Multiset.inter_zero
modified theorem Multiset.le_inter
modified theorem Multiset.le_inter_iff
modified theorem Multiset.le_union_left
modified theorem Multiset.le_union_right
modified theorem Multiset.map_union
modified theorem Multiset.mem_inter
modified theorem Multiset.mem_union
modified theorem Multiset.sub_add_inter
modified theorem Multiset.sub_cons
modified theorem Multiset.sub_eq_fold_erase
modified theorem Multiset.sub_inter
modified theorem Multiset.sup_eq_union
modified def Multiset.union
modified theorem Multiset.union_add_distrib
modified theorem Multiset.union_comm
modified theorem Multiset.union_def
modified theorem Multiset.union_le
modified theorem Multiset.union_le_add
modified theorem Multiset.union_le_iff
modified theorem Multiset.union_zero
modified theorem Multiset.zero_inter
modified theorem Multiset.zero_union