Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-23 23:02 584ae9db

View on Github →

chore(data/{lists,multiset}/*): More dot notation (#12876) Rename many list and multiset lemmas to make them eligible to dot notation. Also add a few aliases to ↔ lemmas for even more dot notation. Renames

Estimated changes

modified def finset.erase
modified def finset.filter
modified theorem finset.image_val_of_inj_on
modified theorem finset.insert_def
modified def finset.map
modified theorem finset.not_mem_erase
modified def alist.erase
modified theorem alist.keys_erase
deleted theorem list.mem_erase_of_nodup
added theorem list.nodup.append
added theorem list.nodup.diff
added theorem list.nodup.erase
added theorem list.nodup.filter
added theorem list.nodup.insert
added theorem list.nodup.inter
added theorem list.nodup.map_on
added theorem list.nodup.not_mem
added theorem list.nodup.of_cons
added theorem list.nodup.of_map
added theorem list.nodup.pmap
added theorem list.nodup.sigma
added theorem list.nodup.union
deleted theorem list.nodup_concat
deleted theorem list.nodup_cons_of_nodup
deleted theorem list.nodup_diff
deleted theorem list.nodup_erase_of_nodup
deleted theorem list.nodup_filter
deleted theorem list.nodup_filter_map
deleted theorem list.nodup_insert
deleted theorem list.nodup_inter_of_nodup
deleted theorem list.nodup_map
deleted theorem list.nodup_map_on
deleted theorem list.nodup_of_nodup_cons
deleted theorem list.nodup_of_nodup_map
deleted theorem list.nodup_of_sublist
deleted theorem list.nodup_pmap
deleted theorem list.nodup_product
deleted theorem list.nodup_sigma
modified theorem list.nodup_singleton
modified theorem list.nodup_sublists_len
deleted theorem list.nodup_union
deleted theorem list.nodup_update_nth
modified theorem list.not_nodup_cons_of_mem
deleted theorem list.forall_of_pairwise
modified theorem list.pairwise.and
added theorem list.pairwise.filter
added theorem list.pairwise.forall
modified theorem list.pairwise.imp
modified theorem list.pairwise.imp₂
added theorem list.pairwise.map
added theorem list.pairwise.of_cons
added theorem list.pairwise.of_map
modified theorem list.pairwise.set_pairwise
added theorem list.pairwise_and_iff
deleted theorem list.pairwise_of_sublist
deleted theorem list.pairwise_sublists'
modified theorem list.pw_filter_idempotent
modified theorem list.rel_of_pairwise_cons
deleted theorem list.kerase_nodupkeys
deleted theorem list.kunion_nodupkeys
deleted theorem list.nodup_of_nodupkeys
added theorem list.nodupkeys.kerase
added theorem list.nodupkeys.kunion
added theorem list.nodupkeys.sublist
deleted theorem list.nodupkeys_of_sublist
added theorem list.sorted.of_cons
added theorem multiset.nodup.ndinter
added theorem multiset.nodup.ndunion
deleted theorem multiset.nodup_ndinsert
deleted theorem multiset.nodup_ndinter
deleted theorem multiset.nodup_ndunion
added theorem multiset.nodup.add_iff
added theorem multiset.nodup.cons
added theorem multiset.nodup.erase
added theorem multiset.nodup.ext
added theorem multiset.nodup.filter
added theorem multiset.nodup.map
added theorem multiset.nodup.map_on
added theorem multiset.nodup.not_mem
added theorem multiset.nodup.of_cons
added theorem multiset.nodup.of_map
added theorem multiset.nodup.pmap
deleted theorem multiset.nodup_ext
deleted theorem multiset.nodup_filter
deleted theorem multiset.nodup_filter_map
deleted theorem multiset.nodup_inter_left
deleted theorem multiset.nodup_map
deleted theorem multiset.nodup_map_on
deleted theorem multiset.nodup_pmap
deleted theorem multiset.nodup_product
deleted theorem multiset.nodup_sigma
deleted theorem multiset.nodup_pi