Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-13 01:46 6db58292

View on Github →

feat(data/finmap): extend the API (#1223)

Estimated changes

added def finmap.all
added def finmap.any
added theorem finmap.disjoint.symm
added def finmap.disjoint
added theorem finmap.disjoint_empty
modified theorem finmap.empty_to_finmap
added theorem finmap.empty_union
added theorem finmap.erase_erase
added theorem finmap.ext_lookup
added theorem finmap.insert_insert
added theorem finmap.insert_union
added theorem finmap.mem_iff
added theorem finmap.mem_singleton
added def finmap.sdiff
added theorem finmap.to_finmap_cons
added theorem finmap.to_finmap_nil
added theorem finmap.union_assoc
added theorem finmap.union_cancel
added theorem finmap.union_empty
added def list.to_finmap
added def alist.disjoint
added theorem alist.entries_to_alist
added theorem alist.erase_erase
added theorem alist.insert_insert
added theorem alist.insert_union
added theorem alist.lookup_to_alist
added theorem alist.to_alist_cons
added theorem alist.union_assoc
added theorem alist.union_erase
added def list.to_alist
added theorem list.foldl_eq_foldr'
added theorem list.foldl_eq_of_comm'
added theorem list.foldr_eq_of_comm'
added theorem list.mem_enum_from
added theorem list.pw_filter_map
added theorem list.kerase_kerase
added theorem list.lookup_ext
added theorem list.mem_ext