Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-22 05:33 902b94d3

View on Github →

refactor(data/finset): redefine finsets as subtype of multisets

Estimated changes

Modified algebra/big_operators.lean

deleted theorem finset.prod_to_finset_of_nodup

Modified analysis/ennreal.lean

Modified analysis/limits.lean

Modified analysis/measure_theory/measure_space.lean

Modified analysis/measure_theory/outer_measure.lean

Modified analysis/topology/continuity.lean

modified structure dense_embedding

Modified analysis/topology/infinite_sum.lean

Modified analysis/topology/topological_structures.lean

Modified data/encodable.lean

Modified data/finset/basic.lean

modified def finset.card

added theorem finset.card_def

added theorem finset.card_eq_zero

modified theorem finset.card_erase_of_mem

modified theorem finset.card_insert_le

modified theorem finset.card_insert_of_not_mem

added theorem finset.card_pos

modified theorem finset.card_range

modified theorem finset.empty_inter

modified theorem finset.empty_subset

modified theorem finset.empty_union

added theorem finset.empty_val

deleted theorem finset.eq_empty_of_card_eq_zero

modified theorem finset.eq_empty_of_forall_not_mem

deleted theorem finset.eq_empty_of_subset_empty

added theorem finset.eq_of_veq

modified def finset.erase

added theorem finset.erase_dup_eq_self

deleted theorem finset.erase_dup_map_erase_dup_eq

modified theorem finset.erase_empty

modified theorem finset.erase_eq_of_not_mem

modified theorem finset.erase_insert

modified theorem finset.erase_insert_subset

modified theorem finset.erase_subset

modified theorem finset.erase_subset_erase

deleted theorem finset.erase_subset_of_subset_insert

added theorem finset.erase_val

modified theorem finset.exists_mem_of_ne_empty

modified theorem finset.exists_nat_subset_range

modified theorem finset.ext

added def finset.filter

added theorem finset.filter_and

modified theorem finset.filter_false

modified theorem finset.filter_filter

modified theorem finset.filter_inter_filter_neg_eq

added theorem finset.filter_not

added theorem finset.filter_or

modified theorem finset.filter_subset

modified theorem finset.filter_union

modified theorem finset.filter_union_filter_neg_eq

added theorem finset.filter_val

deleted theorem finset.forall_of_forall_insert

added theorem finset.has_insert_eq_insert

added def finset.image

modified theorem finset.image_empty

added theorem finset.image_eq_empty

deleted theorem finset.image_eq_empty_iff

modified theorem finset.image_filter

modified theorem finset.image_id

modified theorem finset.image_image

modified theorem finset.image_insert

modified theorem finset.image_inter

modified theorem finset.image_singleton

modified theorem finset.image_subset_image

modified theorem finset.image_to_finset

deleted theorem finset.image_to_finset_of_nodup

modified theorem finset.image_union

added theorem finset.image_val

added theorem finset.image_val_of_inj_on

modified theorem finset.insert.comm

added theorem finset.insert_def

modified theorem finset.insert_eq

modified theorem finset.insert_eq_of_mem

modified theorem finset.insert_erase

modified theorem finset.insert_erase_subset

modified theorem finset.insert_idem

modified theorem finset.insert_ne_empty

modified theorem finset.insert_singelton_self_eq

added theorem finset.insert_subset

modified theorem finset.insert_subset_insert

modified theorem finset.insert_union

added theorem finset.insert_val'

added theorem finset.insert_val

modified theorem finset.inter_assoc

modified theorem finset.inter_comm

modified theorem finset.inter_empty

modified theorem finset.inter_left_comm

modified theorem finset.inter_right_comm

added theorem finset.inter_sdiff_self

modified theorem finset.inter_self

modified theorem finset.inter_subset_left

modified theorem finset.inter_subset_right

added theorem finset.inter_val

added theorem finset.inter_val_nd

deleted def finset.mem

added theorem finset.mem_def

modified theorem finset.mem_erase

modified theorem finset.mem_erase_of_ne_of_mem

modified theorem finset.mem_filter

added theorem finset.mem_image

deleted theorem finset.mem_image_iff

added theorem finset.mem_image_of_mem

modified theorem finset.mem_insert

modified theorem finset.mem_insert_of_mem

modified theorem finset.mem_insert_self

modified theorem finset.mem_inter

deleted theorem finset.mem_list_of_mem

modified theorem finset.mem_of_mem_erase

modified theorem finset.mem_of_mem_insert_of_ne

modified theorem finset.mem_of_mem_inter_left

modified theorem finset.mem_of_mem_inter_right

deleted theorem finset.mem_of_mem_list

added theorem finset.mem_of_subset

deleted theorem finset.mem_of_subset_of_mem

deleted theorem finset.mem_or_mem_of_mem_union

modified theorem finset.mem_range

added theorem finset.mem_sdiff

deleted theorem finset.mem_sdiff_iff

modified theorem finset.mem_singleton

modified theorem finset.mem_singleton_self

deleted theorem finset.mem_to_finset

deleted theorem finset.mem_to_finset_of_mem

deleted theorem finset.mem_to_finset_of_nodup_eq

modified theorem finset.mem_union

modified theorem finset.mem_union_left

modified theorem finset.mem_union_right

added theorem finset.mem_univ

deleted theorem finset.ne_empty_of_card_eq_succ

added theorem finset.ne_empty_of_mem

modified theorem finset.ne_of_mem_erase

modified theorem finset.not_mem_empty

modified theorem finset.not_mem_erase

modified theorem finset.not_mem_range_self

modified def finset.range

modified theorem finset.range_subset

modified theorem finset.range_succ

added theorem finset.range_val

added theorem finset.sdiff_eq_filter

modified theorem finset.sdiff_inter_self

modified theorem finset.sdiff_subset_sdiff

modified theorem finset.sdiff_union_of_subset

modified theorem finset.singleton_inj

modified theorem finset.singleton_ne_empty

added theorem finset.singleton_val

modified theorem finset.subset.refl

modified theorem finset.subset.trans

added theorem finset.subset_def

added theorem finset.subset_empty

deleted theorem finset.subset_empty_iff

modified theorem finset.subset_iff

modified theorem finset.subset_insert

modified theorem finset.subset_insert_iff

deleted theorem finset.subset_insert_of_erase_subset

modified theorem finset.subset_union_left

modified theorem finset.subset_union_right

added theorem finset.subset_univ

deleted def finset.to_finset

deleted theorem finset.to_finset_eq_of_nodup

deleted def finset.to_finset_of_nodup

modified theorem finset.union_assoc

modified theorem finset.union_comm

modified theorem finset.union_empty

modified theorem finset.union_idempotent

modified theorem finset.union_insert

modified theorem finset.union_left_comm

modified theorem finset.union_right_comm

added theorem finset.union_sdiff_of_subset

modified theorem finset.union_self

modified theorem finset.union_subset

added theorem finset.union_val

added theorem finset.union_val_nd

added def finset.univ

added theorem finset.val_eq_zero

added theorem finset.val_inj

added theorem finset.val_le_iff

added structure finset

added def fintype.of_list

added def fintype.of_multiset

added theorem list.mem_to_finset

added def list.to_finset

added theorem list.to_finset_eq

added theorem list.to_finset_val

added theorem multiset.mem_to_finset

added def multiset.to_finset

added theorem multiset.to_finset_eq

added theorem multiset.to_finset_val

deleted def nodup_list

deleted def to_nodup_list

deleted def to_nodup_list_of_nodup

deleted def {u}

Modified data/finset/fold.lean

modified theorem finset.bind_empty

modified theorem finset.bind_image

modified theorem finset.bind_insert

added theorem finset.bind_to_finset

modified def finset.fold

modified theorem finset.fold_congr

modified theorem finset.fold_empty

modified theorem finset.fold_hom

modified theorem finset.fold_image

modified theorem finset.fold_insert

modified theorem finset.fold_insert_idem

modified theorem finset.fold_op_distrib

modified theorem finset.fold_singleton

deleted theorem finset.fold_to_finset_of_nodup

modified theorem finset.fold_union_inter

modified theorem finset.image_bind

added theorem finset.mem_bind

deleted theorem finset.mem_bind_iff

added theorem finset.mem_product

deleted theorem finset.mem_product_iff

added theorem finset.mem_sigma

deleted theorem finset.mem_sigma_iff

added theorem finset.product_eq_bind

added theorem finset.product_val

modified theorem finset.sigma_mono

Modified data/list/basic.lean

added theorem list.map_sublist_map

added theorem list.range_concat

Modified data/multiset/basic.lean

modified theorem multiset.add_inter_distrib

modified theorem multiset.add_union_distrib

added theorem multiset.card_eq_zero

added theorem multiset.card_pos

added theorem multiset.coe_fold_l

added theorem multiset.coe_fold_r

added theorem multiset.cons_inter_distrib

added theorem multiset.cons_union_distrib

added theorem multiset.erase_dup_cons

added theorem multiset.erase_dup_ext

added theorem multiset.erase_dup_map_erase_dup_eq

added theorem multiset.erase_dup_subset'

added def multiset.fold

added theorem multiset.fold_add

added theorem multiset.fold_cons'_left

added theorem multiset.fold_cons'_right

added theorem multiset.fold_cons_left

added theorem multiset.fold_cons_right

added theorem multiset.fold_distrib

added theorem multiset.fold_eq_foldl

added theorem multiset.fold_eq_foldr

added theorem multiset.fold_erase_dup_idem

added theorem multiset.fold_hom

added theorem multiset.fold_singleton

added theorem multiset.fold_union_inter

added theorem multiset.fold_zero

modified theorem multiset.inter_add_distrib

added theorem multiset.map_congr

added theorem multiset.map_le_map

added theorem multiset.map_subset_map

added theorem multiset.mem_bind

added theorem multiset.mem_join

added theorem multiset.mem_product

added theorem multiset.mem_sub_of_nodup

modified theorem multiset.nodup_erase_dup

added theorem multiset.nodup_inter_left

deleted theorem multiset.nodup_inter_of_nodup

added theorem multiset.nodup_inter_right

modified theorem multiset.nodup_ndinsert

added theorem multiset.nodup_union

added theorem multiset.product_singleton

added theorem multiset.range_succ

added theorem multiset.range_zero

added theorem multiset.singleton_le

added theorem multiset.subset_erase_dup'

added theorem multiset.subset_zero

deleted theorem multiset.subset_zero_iff

modified theorem multiset.union_add_distrib

Modified data/nat/basic.lean

modified theorem nat.sub_le_right_iff_le_add

Modified data/set/countable.lean

Modified order/filter.lean