Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-27 13:33 f2b4d2e8

View on Github →

refactor(data/finset): use generic set notation for finsets

Estimated changes

modified theorem finset.erase_insert
modified theorem finset.erase_insert_subset
modified theorem finset.exists_mem_empty_iff
modified theorem finset.forall_mem_empty_iff
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
modified theorem finset.mem_insert
modified theorem finset.mem_insert_iff
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
modified theorem finset.pair_eq_singleton
modified theorem finset.singleton_ne_empty
modified theorem finset.upto_succ