Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-23 23:33 16d40d74

View on Github →

feat(data/finset): fintype, multiset.sort, list.pmap

Estimated changes

Modified algebra/big_operators.lean

modified theorem finset.prod_bind

modified theorem finset.prod_product

Modified analysis/measure_theory/outer_measure.lean

Modified analysis/topology/continuity.lean

Modified data/encodable.lean

Modified data/equiv.lean

modified theorem equiv.apply_eq_iff_eq

modified theorem equiv.apply_eq_iff_eq_inverse_apply

modified theorem equiv.apply_inverse_apply

added def equiv.arrow_empty_unit

deleted theorem equiv.arrow_empty_unit

modified theorem equiv.coe_fn_mk

modified theorem equiv.coe_fn_symm_mk

modified theorem equiv.comp_apply

added def equiv.empty_of_not_nonempty

deleted theorem equiv.empty_of_not_nonempty

deleted theorem equiv.eq_iff_eq_of_injective

modified theorem equiv.eq_of_to_fun_eq

modified theorem equiv.id_apply

modified theorem equiv.inverse_apply_apply

added def equiv.sum_equiv_sigma_bool

modified theorem equiv.swap_apply_def

modified theorem equiv.swap_apply_left

modified theorem equiv.swap_apply_of_ne_of_ne

modified theorem equiv.swap_apply_right

modified theorem equiv.swap_comm

modified theorem equiv.swap_comp_apply

modified theorem equiv.swap_core_comm

modified theorem equiv.swap_core_self

modified theorem equiv.swap_core_swap_core

modified theorem equiv.swap_self

modified theorem equiv.swap_swap

modified theorem function.left_inverse.f_g_eq_id

modified theorem function.right_inverse.g_f_eq_id

modified theorem subtype.map_comp

modified theorem subtype.map_id

Modified data/finset/basic.lean

added def finset.attach

added theorem finset.attach_val

added theorem finset.bind_empty

added theorem finset.bind_image

added theorem finset.bind_insert

added theorem finset.bind_to_finset

added theorem finset.bind_val

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_insert_idem

added theorem finset.fold_op_distrib

added theorem finset.fold_singleton

added theorem finset.fold_union_inter

added theorem finset.image_bind

added theorem finset.mem_attach

added theorem finset.mem_bind

added theorem finset.mem_mk

added theorem finset.mem_product

added theorem finset.mem_sigma

deleted theorem finset.mem_univ

added theorem finset.product_eq_bind

added theorem finset.product_val

added theorem finset.sigma_eq_bind

added theorem finset.sigma_mono

added def finset.sort

added theorem finset.sort_eq

added theorem finset.sort_nodup

added theorem finset.sort_sorted

added theorem finset.sort_to_finset

deleted theorem finset.subset_univ

deleted def finset.univ

deleted def fintype.of_list

deleted def fintype.of_multiset

Modified data/finset/default.lean

Created data/finset/fintype.lean

added theorem finset.mem_univ

added theorem finset.subset_univ

added def finset.univ

added def fintype.of_bijective

added def fintype.of_equiv

added def fintype.of_list

added def fintype.of_multiset

added def fintype.of_surjective

Deleted data/finset/fold.lean

deleted theorem finset.bind_empty

deleted theorem finset.bind_image

deleted theorem finset.bind_insert

deleted theorem finset.bind_to_finset

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_op_distrib

deleted theorem finset.fold_singleton

deleted theorem finset.fold_union_inter

deleted theorem finset.image_bind

deleted theorem finset.mem_bind

deleted theorem finset.mem_product

deleted theorem finset.mem_sigma

deleted theorem finset.product_eq_bind

deleted theorem finset.product_val

deleted theorem finset.sigma_mono

Modified data/list/basic.lean

added def list.attach

added theorem list.attach_map_val

added theorem list.length_sigma

added theorem list.map_pmap

added theorem list.mem_attach

added theorem list.mem_pmap

added theorem list.mem_sigma

added theorem list.nil_sigma

added theorem list.nodup_attach

added theorem list.nodup_pmap

added theorem list.nodup_sigma

added def list.pmap

added theorem list.pmap_congr

added theorem list.pmap_eq_map

added theorem list.pmap_eq_map_attach

added def list.sigma

added theorem list.sigma_cons

added theorem list.sigma_nil

Modified data/list/perm.lean

added theorem list.perm_pmap

Modified data/list/sort.lean

modified def list.split

Modified data/multiset/basic.lean

added theorem multiset.add_sigma

added def multiset.attach

added theorem multiset.attach_map_val

added theorem multiset.coe_attach

added theorem multiset.coe_pmap

added theorem multiset.coe_sigma

added theorem multiset.coe_sort

added theorem multiset.cons_sigma

added theorem multiset.count_smul

added theorem multiset.le_smul_erase_dup

added theorem multiset.map_pmap

added theorem multiset.mem_attach

added theorem multiset.mem_pmap

added theorem multiset.mem_sigma

added theorem multiset.nodup_attach

added theorem multiset.nodup_pmap

added theorem multiset.nodup_sigma

added def multiset.pmap

added theorem multiset.pmap_congr

added theorem multiset.pmap_eq_map

added theorem multiset.pmap_eq_map_attach

added theorem multiset.prod_repeat

added theorem multiset.sigma_add

added theorem multiset.sigma_singleton

added def multiset.sort

added theorem multiset.sort_eq

added theorem multiset.sort_sorted

added theorem multiset.zero_sigma

Modified logic/basic.lean

modified theorem and_iff_left_of_imp

modified theorem and_iff_right_of_imp

modified theorem classical.cases

modified theorem classical.or_not

modified theorem false_neq_true

modified theorem forall_2_true_iff

modified theorem forall_3_true_iff

modified theorem forall_true_iff'

modified theorem heq_iff_eq

Modified logic/function.lean

added def function.injective.decidable_eq

modified theorem function.injective.eq_iff