Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-04 08:09 6f72c228

View on Github →

chore(data/finset): add a few lemmas (#4901)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.insert_sdiff_insert

added theorem finset.piecewise_idem_left

added theorem finset.piecewise_idem_right

added theorem finset.piecewise_mem_Icc'

added theorem finset.piecewise_mem_Icc

added theorem finset.piecewise_mem_Icc_of_mem_of_mem

added theorem finset.piecewise_piecewise_of_subset_left

added theorem finset.piecewise_piecewise_of_subset_right

added theorem finset.sdiff_insert_of_not_mem