Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-11 16:11 bde8690e

View on Github →

feat(data/alist,data/finmap): union (#750)

Estimated changes

added theorem alist.empty_entries
added theorem alist.empty_union
added theorem alist.lookup_empty
modified theorem alist.lookup_insert_ne
modified theorem alist.mem_insert
added theorem alist.mem_lookup_union
added theorem alist.mem_union
added theorem alist.perm_union
added def alist.union
added theorem alist.union_empty
added theorem alist.union_entries
added theorem list.kerase_comm
added def list.kunion
added theorem list.kunion_cons
added theorem list.kunion_kerase
added theorem list.kunion_nil
added theorem list.kunion_nodupkeys
modified theorem list.lookup_kinsert_ne
modified theorem list.mem_keys_kinsert
added theorem list.mem_keys_kunion
added theorem list.mem_lookup_kunion
added theorem list.nil_kunion
added theorem list.perm_kunion
added theorem list.perm_kunion_left
added theorem list.perm_kunion_right