Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-27 20:57 c17d11b7

View on Github →

fix(data/finset): use the type class projections for insert; hide most constants using protected; add image of finset

Estimated changes

Modified data/finset/basic.lean

modified theorem finset.card_empty

deleted def finset.empty

modified theorem finset.empty_inter

modified theorem finset.empty_subset

modified theorem finset.empty_union

modified theorem finset.eq_empty_of_subset_empty

modified theorem finset.eq_of_mem_singleton

modified theorem finset.eq_of_singleton_eq

added theorem finset.erase_dup_map_erase_dup_eq

modified theorem finset.erase_insert

modified theorem finset.erase_insert_subset

added theorem finset.image_id

added theorem finset.image_image

added theorem finset.image_to_finset

added theorem finset.image_to_finset_of_nodup

modified theorem finset.insert.comm

deleted def finset.insert

modified theorem finset.insert_eq

modified theorem finset.insert_eq_of_mem

added theorem finset.insert_inter_of_mem

added theorem finset.insert_inter_of_not_mem

modified theorem finset.insert_subset_insert

modified theorem finset.insert_union

deleted def finset.inter

modified theorem finset.inter_empty

modified theorem finset.mem_insert

modified theorem finset.mem_insert_iff

modified theorem finset.mem_singleton_iff

modified theorem finset.perm_insert_cons_of_not_mem

modified theorem finset.singleton_inter_of_mem

modified theorem finset.singleton_inter_of_not_mem

deleted def finset.subset

deleted def finset.subset_aux

modified theorem finset.subset_empty_iff

deleted def finset.union

modified theorem finset.union_empty

modified theorem finset.upto_succ

modified theorem finset.upto_zero

modified def to_nodup_list_of_nodup

Modified data/list/set.lean

modified theorem list.length_erase_of_not_mem

modified theorem list.nodup_map

added theorem list.nodup_map_on