Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-18 10:15 0a794fac

View on Github →

feat(data/finset): new union, set difference, singleton lemmas (#1702)

Singleton iff unique element lemma
Set difference lemmas
Changes from review

Estimated changes

Modified src/data/finset.lean

added theorem finset.eq_singleton_iff_unique_mem

added theorem finset.sdiff_eq_empty_iff_subset

added theorem finset.sdiff_union_self_eq_union

added theorem finset.singleton_iff_unique_mem

added theorem finset.union_sdiff_self_eq_union

added theorem finset.union_sdiff_symm