Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-01 10:05 7bd19b32

View on Github →

chore(data/finset, data/multiset): split into smaller files (#3256) This follows on from #2341, which split the second half of data.list.basic into separate files. This now does the same (trying to follow a similar split) for data.multiset and data.finset.

Estimated changes

deleted theorem finset.Ico.card
deleted theorem finset.Ico.diff_left
deleted theorem finset.Ico.diff_right
deleted theorem finset.Ico.eq_empty_iff
deleted theorem finset.Ico.eq_empty_of_le
deleted theorem finset.Ico.filter_le
deleted theorem finset.Ico.filter_lt
deleted theorem finset.Ico.image_add
deleted theorem finset.Ico.image_sub
deleted theorem finset.Ico.mem
deleted theorem finset.Ico.not_mem_top
deleted theorem finset.Ico.pred_singleton
deleted theorem finset.Ico.self_eq_empty
deleted theorem finset.Ico.subset_iff
deleted theorem finset.Ico.succ_singleton
deleted theorem finset.Ico.succ_top'
deleted theorem finset.Ico.succ_top
deleted theorem finset.Ico.to_finset
deleted theorem finset.Ico.val
deleted theorem finset.Ico.zero_bot
deleted def finset.Ico
deleted theorem finset.Ico_ℤ.card
deleted theorem finset.Ico_ℤ.mem
deleted def finset.Ico_ℤ
deleted theorem finset.bInter_coe
deleted theorem finset.bInter_insert
deleted theorem finset.bInter_inter
deleted theorem finset.bInter_singleton
deleted theorem finset.bUnion_coe
deleted theorem finset.bUnion_insert
deleted theorem finset.bUnion_singleton
deleted theorem finset.bUnion_union
deleted theorem finset.card_powerset
deleted theorem finset.card_powerset_len
deleted theorem finset.empty_mem_powerset
deleted theorem finset.exists_max_image
deleted theorem finset.exists_min_image
deleted def finset.fold
deleted theorem finset.fold_congr
deleted theorem finset.fold_empty
deleted theorem finset.fold_hom
deleted theorem finset.fold_image
deleted theorem finset.fold_insert
deleted theorem finset.fold_insert_idem
deleted theorem finset.fold_map
deleted theorem finset.fold_max_le
deleted theorem finset.fold_max_lt
deleted theorem finset.fold_min_le
deleted theorem finset.fold_min_lt
deleted theorem finset.fold_op_distrib
deleted theorem finset.fold_op_rel_iff_or
deleted theorem finset.fold_singleton
deleted theorem finset.fold_union_inter
deleted def finset.inf
deleted theorem finset.inf_congr
deleted theorem finset.inf_empty
deleted theorem finset.inf_eq_infi
deleted theorem finset.inf_insert
deleted theorem finset.inf_le
deleted theorem finset.inf_mono
deleted theorem finset.inf_mono_fun
deleted theorem finset.inf_singleton
deleted theorem finset.inf_union
deleted theorem finset.inf_val
deleted theorem finset.infi_coe
deleted theorem finset.infi_finset_image
deleted theorem finset.infi_insert
deleted theorem finset.infi_singleton
deleted theorem finset.infi_union
deleted theorem finset.le_fold_max
deleted theorem finset.le_fold_min
deleted theorem finset.le_inf
deleted theorem finset.le_inf_iff
deleted theorem finset.le_max'
deleted theorem finset.le_max_of_mem
deleted theorem finset.le_min'
deleted theorem finset.le_sup
deleted theorem finset.length_sort
deleted theorem finset.lt_fold_max
deleted theorem finset.lt_fold_min
deleted theorem finset.lt_inf_iff
deleted def finset.max'
deleted theorem finset.max'_le
deleted theorem finset.max'_mem
deleted theorem finset.max_empty
deleted theorem finset.max_eq_none
deleted theorem finset.max_insert
deleted theorem finset.max_of_mem
deleted theorem finset.max_of_nonempty
deleted theorem finset.max_singleton
deleted theorem finset.mem_of_max
deleted theorem finset.mem_of_min
deleted theorem finset.mem_pi
deleted theorem finset.mem_powerset
deleted theorem finset.mem_powerset_len
deleted theorem finset.mem_powerset_self
deleted theorem finset.mem_sort
deleted def finset.min'
deleted theorem finset.min'_le
deleted theorem finset.min'_lt_max'
deleted theorem finset.min'_mem
deleted theorem finset.min_empty
deleted theorem finset.min_eq_none
deleted theorem finset.min_insert
deleted theorem finset.min_le_of_mem
deleted theorem finset.min_of_mem
deleted theorem finset.min_of_nonempty
deleted theorem finset.min_singleton
deleted def finset.mono_of_fin
deleted theorem finset.mono_of_fin_bij_on
deleted theorem finset.mono_of_fin_last
deleted theorem finset.mono_of_fin_unique
deleted theorem finset.mono_of_fin_zero
deleted def finset.pi.cons
deleted theorem finset.pi.cons_ne
deleted theorem finset.pi.cons_same
deleted def finset.pi.empty
deleted def finset.pi
deleted theorem finset.pi_cons_injective
deleted theorem finset.pi_empty
deleted theorem finset.pi_insert
deleted theorem finset.pi_subset
deleted theorem finset.pi_val
deleted def finset.powerset
deleted theorem finset.powerset_empty
deleted theorem finset.powerset_insert
deleted def finset.powerset_len
deleted theorem finset.powerset_len_mono
deleted theorem finset.powerset_mono
deleted theorem finset.range_eq_Ico
deleted def finset.sort
deleted theorem finset.sort_eq
deleted theorem finset.sort_nodup
deleted theorem finset.sort_sorted
deleted theorem finset.sort_sorted_lt
deleted theorem finset.sort_to_finset
deleted def finset.sup
deleted theorem finset.sup_congr
deleted theorem finset.sup_def
deleted theorem finset.sup_empty
deleted theorem finset.sup_eq_supr
deleted theorem finset.sup_insert
deleted theorem finset.sup_le
deleted theorem finset.sup_le_iff
deleted theorem finset.sup_lt_iff
deleted theorem finset.sup_mono
deleted theorem finset.sup_mono_fun
deleted theorem finset.sup_singleton
deleted theorem finset.sup_union
deleted theorem finset.supr_coe
deleted theorem finset.supr_finset_image
deleted theorem finset.supr_insert
deleted theorem finset.supr_singleton
deleted theorem finset.supr_union
deleted theorem infi_eq_infi_finset
deleted theorem multiset.count_sup
deleted theorem set.Inter_eq_Inter_finset
deleted theorem set.Union_eq_Union_finset
deleted theorem supr_eq_supr_finset
added def finset.fold
added theorem finset.fold_congr
added theorem finset.fold_empty
added theorem finset.fold_hom
added theorem finset.fold_image
added theorem finset.fold_insert
added theorem finset.fold_map
added theorem finset.fold_max_le
added theorem finset.fold_max_lt
added theorem finset.fold_min_le
added theorem finset.fold_min_lt
added theorem finset.fold_op_distrib
added theorem finset.fold_singleton
added theorem finset.le_fold_max
added theorem finset.le_fold_min
added theorem finset.lt_fold_max
added theorem finset.lt_fold_min
added theorem finset.Ico.card
added theorem finset.Ico.diff_left
added theorem finset.Ico.diff_right
added theorem finset.Ico.filter_le
added theorem finset.Ico.filter_lt
added theorem finset.Ico.image_add
added theorem finset.Ico.image_sub
added theorem finset.Ico.mem
added theorem finset.Ico.not_mem_top
added theorem finset.Ico.subset_iff
added theorem finset.Ico.succ_top'
added theorem finset.Ico.succ_top
added theorem finset.Ico.to_finset
added theorem finset.Ico.val
added theorem finset.Ico.zero_bot
added def finset.Ico
added theorem finset.Ico_ℤ.card
added theorem finset.Ico_ℤ.mem
added def finset.Ico_ℤ
added theorem finset.range_eq_Ico
added theorem finset.bInter_coe
added theorem finset.bInter_insert
added theorem finset.bInter_inter
added theorem finset.bUnion_coe
added theorem finset.bUnion_insert
added theorem finset.bUnion_union
added def finset.inf
added theorem finset.inf_congr
added theorem finset.inf_empty
added theorem finset.inf_eq_infi
added theorem finset.inf_insert
added theorem finset.inf_le
added theorem finset.inf_mono
added theorem finset.inf_mono_fun
added theorem finset.inf_singleton
added theorem finset.inf_union
added theorem finset.inf_val
added theorem finset.infi_coe
added theorem finset.infi_insert
added theorem finset.infi_singleton
added theorem finset.infi_union
added theorem finset.le_inf
added theorem finset.le_inf_iff
added theorem finset.le_max'
added theorem finset.le_max_of_mem
added theorem finset.le_min'
added theorem finset.le_sup
added theorem finset.lt_inf_iff
added def finset.max'
added theorem finset.max'_le
added theorem finset.max'_mem
added theorem finset.max_empty
added theorem finset.max_eq_none
added theorem finset.max_insert
added theorem finset.max_of_mem
added theorem finset.max_of_nonempty
added theorem finset.max_singleton
added theorem finset.mem_of_max
added theorem finset.mem_of_min
added def finset.min'
added theorem finset.min'_le
added theorem finset.min'_lt_max'
added theorem finset.min'_mem
added theorem finset.min_empty
added theorem finset.min_eq_none
added theorem finset.min_insert
added theorem finset.min_le_of_mem
added theorem finset.min_of_mem
added theorem finset.min_of_nonempty
added theorem finset.min_singleton
added def finset.sup
added theorem finset.sup_congr
added theorem finset.sup_def
added theorem finset.sup_empty
added theorem finset.sup_eq_supr
added theorem finset.sup_insert
added theorem finset.sup_le
added theorem finset.sup_le_iff
added theorem finset.sup_lt_iff
added theorem finset.sup_mono
added theorem finset.sup_mono_fun
added theorem finset.sup_singleton
added theorem finset.sup_union
added theorem finset.supr_coe
added theorem finset.supr_insert
added theorem finset.supr_singleton
added theorem finset.supr_union
added theorem infi_eq_infi_finset
added theorem multiset.count_sup
added theorem supr_eq_supr_finset
added theorem finset.mem_pi
added def finset.pi.cons
added theorem finset.pi.cons_ne
added theorem finset.pi.cons_same
added def finset.pi.empty
added def finset.pi
added theorem finset.pi_empty
added theorem finset.pi_insert
added theorem finset.pi_subset
added theorem finset.pi_val
added theorem finset.card_powerset
added theorem finset.mem_powerset
added def finset.powerset
added theorem finset.powerset_empty
added theorem finset.powerset_insert
added theorem finset.powerset_mono
added theorem finset.length_sort
added theorem finset.mem_sort
added def finset.sort
added theorem finset.sort_eq
added theorem finset.sort_nodup
added theorem finset.sort_sorted
added theorem finset.sort_sorted_lt
added theorem finset.sort_to_finset
added theorem multiset.prod_map_add
deleted theorem multiset.Ico.card
deleted theorem multiset.Ico.eq_cons
deleted theorem multiset.Ico.eq_zero_iff
deleted theorem multiset.Ico.filter_le
deleted theorem multiset.Ico.filter_lt
deleted theorem multiset.Ico.map_add
deleted theorem multiset.Ico.map_sub
deleted theorem multiset.Ico.mem
deleted theorem multiset.Ico.nodup
deleted theorem multiset.Ico.not_mem_top
deleted theorem multiset.Ico.self_eq_zero
deleted theorem multiset.Ico.succ_top
deleted theorem multiset.Ico.zero_bot
deleted def multiset.Ico
deleted theorem multiset.antidiagonal_coe
deleted theorem multiset.attach_ndinsert
deleted theorem multiset.bind_def
deleted theorem multiset.card_pi
deleted theorem multiset.card_powerset
deleted theorem multiset.card_sections
deleted theorem multiset.coe_erase_dup
deleted theorem multiset.coe_fold_l
deleted theorem multiset.coe_fold_r
deleted theorem multiset.coe_ndinsert
deleted theorem multiset.coe_ndinter
deleted theorem multiset.coe_ndunion
deleted theorem multiset.coe_nodup
deleted theorem multiset.coe_sections
deleted theorem multiset.coe_sort
deleted theorem multiset.comp_traverse
deleted theorem multiset.cons_ndunion
deleted def multiset.erase_dup
deleted theorem multiset.erase_dup_add
deleted theorem multiset.erase_dup_cons
deleted theorem multiset.erase_dup_ext
deleted theorem multiset.erase_dup_le
deleted theorem multiset.erase_dup_subset
deleted theorem multiset.erase_dup_zero
deleted theorem multiset.fmap_def
deleted def multiset.fold
deleted theorem multiset.fold_add
deleted theorem multiset.fold_cons'_left
deleted theorem multiset.fold_cons'_right
deleted theorem multiset.fold_cons_left
deleted theorem multiset.fold_cons_right
deleted theorem multiset.fold_distrib
deleted theorem multiset.fold_eq_foldl
deleted theorem multiset.fold_eq_foldr
deleted theorem multiset.fold_hom
deleted theorem multiset.fold_singleton
deleted theorem multiset.fold_union_inter
deleted theorem multiset.fold_zero
deleted theorem multiset.id_traverse
deleted def multiset.inf
deleted theorem multiset.inf_add
deleted theorem multiset.inf_cons
deleted theorem multiset.inf_erase_dup
deleted theorem multiset.inf_le
deleted theorem multiset.inf_mono
deleted theorem multiset.inf_ndinsert
deleted theorem multiset.inf_ndunion
deleted theorem multiset.inf_singleton
deleted theorem multiset.inf_union
deleted theorem multiset.inf_zero
deleted theorem multiset.inter_le_ndinter
deleted theorem multiset.le_erase_dup
deleted theorem multiset.le_iff_subset
deleted theorem multiset.le_inf
deleted theorem multiset.le_ndinsert_self
deleted theorem multiset.le_ndinter
deleted theorem multiset.le_ndunion_left
deleted theorem multiset.le_ndunion_right
deleted theorem multiset.le_sup
deleted theorem multiset.length_sort
deleted theorem multiset.lift_beta
deleted theorem multiset.map_comp_coe
deleted theorem multiset.map_traverse
deleted theorem multiset.mem_antidiagonal
deleted theorem multiset.mem_erase_dup
deleted theorem multiset.mem_ndinsert
deleted theorem multiset.mem_ndinter
deleted theorem multiset.mem_ndunion
deleted theorem multiset.mem_pi
deleted theorem multiset.mem_powerset
deleted theorem multiset.mem_powerset_aux
deleted theorem multiset.mem_powerset_len
deleted theorem multiset.mem_sections
deleted theorem multiset.mem_sort
deleted theorem multiset.mem_sub_of_nodup
deleted theorem multiset.naturality
deleted def multiset.ndinsert
deleted theorem multiset.ndinsert_le
deleted theorem multiset.ndinsert_of_mem
deleted theorem multiset.ndinsert_zero
deleted def multiset.ndinter
deleted theorem multiset.ndinter_eq_inter
deleted theorem multiset.ndinter_le_left
deleted theorem multiset.ndinter_le_right
deleted def multiset.ndunion
deleted theorem multiset.ndunion_eq_union
deleted theorem multiset.ndunion_le
deleted theorem multiset.ndunion_le_add
deleted theorem multiset.ndunion_le_union
deleted def multiset.nodup
deleted theorem multiset.nodup_add
deleted theorem multiset.nodup_attach
deleted theorem multiset.nodup_bind
deleted theorem multiset.nodup_cons
deleted theorem multiset.nodup_erase_dup
deleted theorem multiset.nodup_ext
deleted theorem multiset.nodup_filter
deleted theorem multiset.nodup_filter_map
deleted theorem multiset.nodup_iff_le
deleted theorem multiset.nodup_inter_left
deleted theorem multiset.nodup_map
deleted theorem multiset.nodup_map_on
deleted theorem multiset.nodup_ndinsert
deleted theorem multiset.nodup_ndinter
deleted theorem multiset.nodup_ndunion
deleted theorem multiset.nodup_of_le
deleted theorem multiset.nodup_pi
deleted theorem multiset.nodup_pmap
deleted theorem multiset.nodup_powerset
deleted theorem multiset.nodup_product
deleted theorem multiset.nodup_range
deleted theorem multiset.nodup_sigma
deleted theorem multiset.nodup_singleton
deleted theorem multiset.nodup_union
deleted theorem multiset.nodup_zero
deleted theorem multiset.not_nodup_pair
deleted def multiset.pi.cons
deleted theorem multiset.pi.cons_ne
deleted theorem multiset.pi.cons_same
deleted theorem multiset.pi.cons_swap
deleted def multiset.pi.empty
deleted def multiset.pi
deleted theorem multiset.pi_cons
deleted theorem multiset.pi_zero
deleted def multiset.powerset
deleted theorem multiset.powerset_coe'
deleted theorem multiset.powerset_coe
deleted theorem multiset.powerset_cons
deleted theorem multiset.powerset_len_coe
deleted theorem multiset.powerset_zero
deleted theorem multiset.prod_map_add
deleted theorem multiset.prod_map_sum
deleted theorem multiset.pure_def
deleted theorem multiset.range_le
deleted def multiset.sections
deleted theorem multiset.sections_add
deleted theorem multiset.sections_cons
deleted theorem multiset.sections_zero
deleted def multiset.sort
deleted theorem multiset.sort_eq
deleted theorem multiset.sort_sorted
deleted theorem multiset.subset_erase_dup
deleted def multiset.sup
deleted theorem multiset.sup_add
deleted theorem multiset.sup_cons
deleted theorem multiset.sup_erase_dup
deleted theorem multiset.sup_le
deleted theorem multiset.sup_mono
deleted theorem multiset.sup_ndinsert
deleted theorem multiset.sup_ndunion
deleted theorem multiset.sup_singleton
deleted theorem multiset.sup_union
deleted theorem multiset.sup_zero
deleted def multiset.traverse
deleted theorem multiset.traverse_map
deleted theorem multiset.zero_ndinter
deleted theorem multiset.zero_ndunion
added theorem multiset.coe_erase_dup
added theorem multiset.erase_dup_ext
added theorem multiset.erase_dup_le
added theorem multiset.le_erase_dup
added theorem multiset.mem_erase_dup
added theorem multiset.coe_ndinsert
added theorem multiset.coe_ndinter
added theorem multiset.coe_ndunion
added theorem multiset.cons_ndunion
added theorem multiset.erase_dup_add
added theorem multiset.le_ndinter
added theorem multiset.mem_ndinsert
added theorem multiset.mem_ndinter
added theorem multiset.mem_ndunion
added theorem multiset.ndinsert_le
added theorem multiset.ndinsert_zero
added def multiset.ndinter
added def multiset.ndunion
added theorem multiset.ndunion_le
added theorem multiset.nodup_ndinter
added theorem multiset.nodup_ndunion
added theorem multiset.zero_ndinter
added theorem multiset.zero_ndunion
added theorem multiset.coe_fold_l
added theorem multiset.coe_fold_r
added def multiset.fold
added theorem multiset.fold_add
added theorem multiset.fold_distrib
added theorem multiset.fold_eq_foldl
added theorem multiset.fold_eq_foldr
added theorem multiset.fold_hom
added theorem multiset.fold_zero
added theorem multiset.bind_def
added theorem multiset.comp_traverse
added theorem multiset.fmap_def
added theorem multiset.id_traverse
added theorem multiset.lift_beta
added theorem multiset.map_comp_coe
added theorem multiset.map_traverse
added theorem multiset.naturality
added theorem multiset.pure_def
added theorem multiset.traverse_map
added theorem multiset.Ico.card
added theorem multiset.Ico.eq_cons
added theorem multiset.Ico.filter_le
added theorem multiset.Ico.filter_lt
added theorem multiset.Ico.map_add
added theorem multiset.Ico.map_sub
added theorem multiset.Ico.mem
added theorem multiset.Ico.nodup
added theorem multiset.Ico.succ_top
added theorem multiset.Ico.zero_bot
added def multiset.Ico
added def multiset.inf
added theorem multiset.inf_add
added theorem multiset.inf_cons
added theorem multiset.inf_erase_dup
added theorem multiset.inf_le
added theorem multiset.inf_mono
added theorem multiset.inf_ndinsert
added theorem multiset.inf_ndunion
added theorem multiset.inf_singleton
added theorem multiset.inf_union
added theorem multiset.inf_zero
added theorem multiset.le_inf
added theorem multiset.le_sup
added def multiset.sup
added theorem multiset.sup_add
added theorem multiset.sup_cons
added theorem multiset.sup_erase_dup
added theorem multiset.sup_le
added theorem multiset.sup_mono
added theorem multiset.sup_ndinsert
added theorem multiset.sup_ndunion
added theorem multiset.sup_singleton
added theorem multiset.sup_union
added theorem multiset.sup_zero
added theorem multiset.coe_nodup
added theorem multiset.le_iff_subset
added def multiset.nodup
added theorem multiset.nodup_add
added theorem multiset.nodup_attach
added theorem multiset.nodup_bind
added theorem multiset.nodup_cons
added theorem multiset.nodup_ext
added theorem multiset.nodup_filter
added theorem multiset.nodup_iff_le
added theorem multiset.nodup_map
added theorem multiset.nodup_map_on
added theorem multiset.nodup_of_le
added theorem multiset.nodup_pmap
added theorem multiset.nodup_product
added theorem multiset.nodup_range
added theorem multiset.nodup_sigma
added theorem multiset.nodup_union
added theorem multiset.nodup_zero
added theorem multiset.range_le
added theorem multiset.card_pi
added theorem multiset.mem_pi
added theorem multiset.nodup_pi
added def multiset.pi.cons
added theorem multiset.pi.cons_ne
added theorem multiset.pi.cons_same
added theorem multiset.pi.cons_swap
added def multiset.pi
added theorem multiset.pi_cons
added theorem multiset.pi_zero
added theorem multiset.card_powerset
added theorem multiset.mem_powerset
added theorem multiset.powerset_coe'
added theorem multiset.powerset_coe
added theorem multiset.powerset_cons
added theorem multiset.powerset_zero
added theorem multiset.card_sections
added theorem multiset.coe_sections
added theorem multiset.mem_sections
added theorem multiset.prod_map_sum
added theorem multiset.sections_add
added theorem multiset.sections_cons
added theorem multiset.sections_zero
added theorem multiset.coe_sort
added theorem multiset.length_sort
added theorem multiset.mem_sort
added def multiset.sort
added theorem multiset.sort_eq
added theorem multiset.sort_sorted