Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-27 13:33 8dbee5b1

View on Github →

feat(data/finset): add basics for finsets

Estimated changes

Modified data/finset/basic.lean

modified theorem finset.eq_of_mem_singleton

modified theorem finset.eq_of_singleton_eq

modified theorem finset.erase_insert

modified theorem finset.erase_insert_subset

added theorem finset.exists_mem_empty_eq

modified theorem finset.exists_mem_empty_iff

added theorem finset.exists_mem_insert_eq

modified theorem finset.exists_mem_insert_iff

added theorem finset.forall_mem_empty_eq

modified theorem finset.forall_mem_empty_iff

added theorem finset.forall_mem_insert_eq

modified theorem finset.forall_mem_insert_iff

modified theorem finset.forall_of_forall_insert

modified theorem finset.insert.comm

modified theorem finset.insert_eq

modified theorem finset.insert_eq_of_mem

modified theorem finset.insert_subset_insert

modified theorem finset.insert_union

added theorem finset.mem_empty_eq

modified theorem finset.mem_empty_iff

added theorem finset.mem_erase_eq

modified theorem finset.mem_insert

added theorem finset.mem_insert_eq

modified theorem finset.mem_insert_iff

added theorem finset.mem_inter_eq

modified theorem finset.mem_list_of_mem

modified theorem finset.mem_of_mem_list

modified theorem finset.mem_singleton

modified theorem finset.mem_singleton_iff

modified theorem finset.mem_singleton_of_eq

added theorem finset.mem_union_eq

added theorem finset.mem_upto_eq

modified theorem finset.not_mem_empty

modified theorem finset.pair_eq_singleton

modified theorem finset.singleton_ne_empty

modified def finset.subset_aux

modified theorem finset.upto_succ

modified def finset

modified def nodup_list