Commit 2023-02-03 13:20 70430c95

View on Github →

feat: port Data.Finmap (#1591)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finmap.lean

added def AList.toFinmap

added theorem AList.toFinmap_entries

added theorem AList.toFinmap_eq

added theorem Finmap.Disjoint.symm

added theorem Finmap.Disjoint.symm_iff

added def Finmap.Disjoint

added def Finmap.all

added def Finmap.any

added theorem Finmap.disjoint_empty

added theorem Finmap.disjoint_union_left

added theorem Finmap.disjoint_union_right

added theorem Finmap.dlookup_list_toFinmap

added theorem Finmap.empty_toFinmap

added theorem Finmap.empty_union

added def Finmap.erase

added theorem Finmap.erase_erase

added theorem Finmap.erase_toFinmap

added theorem Finmap.erase_union_singleton

added theorem Finmap.ext

added theorem Finmap.ext_iff

added theorem Finmap.ext_lookup

added def Finmap.extract

added theorem Finmap.extract_eq_lookup_erase

added def Finmap.foldl

added theorem Finmap.induction_on

added theorem Finmap.induction_on₂

added theorem Finmap.induction_on₃

added def Finmap.insert

added theorem Finmap.insert_entries_of_neg

added theorem Finmap.insert_insert

added theorem Finmap.insert_insert_of_ne

added theorem Finmap.insert_singleton_eq

added theorem Finmap.insert_toFinmap

added theorem Finmap.insert_union

added def Finmap.keys

added theorem Finmap.keys_empty

added theorem Finmap.keys_erase

added theorem Finmap.keys_erase_toFinset

added theorem Finmap.keys_ext

added theorem Finmap.keys_replace

added theorem Finmap.keys_singleton

added theorem Finmap.keys_union

added theorem Finmap.keys_val

added def Finmap.liftOn

added theorem Finmap.liftOn_toFinmap

added def Finmap.liftOn₂

added theorem Finmap.liftOn₂_toFinmap

added def Finmap.lookup

added theorem Finmap.lookup_empty

added theorem Finmap.lookup_eq_none

added theorem Finmap.lookup_erase

added theorem Finmap.lookup_erase_ne

added theorem Finmap.lookup_insert

added theorem Finmap.lookup_insert_of_ne

added theorem Finmap.lookup_isSome

added theorem Finmap.lookup_singleton_eq

added theorem Finmap.lookup_toFinmap

added theorem Finmap.lookup_union_left

added theorem Finmap.lookup_union_left_of_not_in

added theorem Finmap.lookup_union_right

added theorem Finmap.mem_def

added theorem Finmap.mem_erase

added theorem Finmap.mem_iff

added theorem Finmap.mem_insert

added theorem Finmap.mem_keys

added theorem Finmap.mem_list_toFinmap

added theorem Finmap.mem_lookup_union

added theorem Finmap.mem_lookup_union_middle

added theorem Finmap.mem_of_lookup_eq_some

added theorem Finmap.mem_replace

added theorem Finmap.mem_singleton

added theorem Finmap.mem_toFinmap

added theorem Finmap.mem_union

added theorem Finmap.not_mem_empty

added theorem Finmap.not_mem_erase_self

added def Finmap.replace

added theorem Finmap.replace_toFinmap

added def Finmap.sdiff

added def Finmap.singleton

added theorem Finmap.toFinmap_cons

added theorem Finmap.toFinmap_nil

added def Finmap.union

added theorem Finmap.union_assoc

added theorem Finmap.union_cancel

added theorem Finmap.union_comm_of_disjoint

added theorem Finmap.union_empty

added theorem Finmap.union_toFinmap

added structure Finmap

added def List.toFinmap

added def Multiset.NodupKeys

added theorem Multiset.coe_keys

added theorem Multiset.coe_nodupKeys

added def Multiset.keys