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

Modified src/data/finmap.lean

added theorem finmap.ext_iff

added theorem finmap.induction_on₂

added theorem finmap.induction_on₃

added theorem finmap.keys_union

added theorem finmap.lookup_empty

added theorem finmap.lookup_union_left

added theorem finmap.lookup_union_right

modified theorem finmap.mem_insert

added theorem finmap.mem_lookup_union

added theorem finmap.mem_lookup_union_middle

added theorem finmap.mem_union

added def finmap.union

added theorem finmap.union_to_finmap

Modified src/data/list/alist.lean

added theorem alist.empty_entries

added theorem alist.empty_union

added theorem alist.lookup_empty

modified theorem alist.lookup_insert_ne

added theorem alist.lookup_union_left

added theorem alist.lookup_union_right

modified theorem alist.mem_insert

added theorem alist.mem_lookup_union

added theorem alist.mem_lookup_union_middle

added theorem alist.mem_union

added theorem alist.perm_union

added theorem alist.singleton_entries

added def alist.union

added theorem alist.union_empty

added theorem alist.union_entries

Modified src/data/list/sigma.lean

added theorem list.kerase_append_left

added theorem list.kerase_append_right

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

added theorem list.lookup_kunion_left

added theorem list.lookup_kunion_right

modified theorem list.mem_keys_kinsert

added theorem list.mem_keys_kunion

added theorem list.mem_lookup_kunion

added theorem list.mem_lookup_kunion_middle

added theorem list.nil_kunion

added theorem list.perm_kunion

added theorem list.perm_kunion_left

added theorem list.perm_kunion_right