Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-30 00:14 413b4263

View on Github →

feat(finset/basic): fill in holes in the finset API (#7386) add basic lemmas about finsets

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.attach_eq_empty_iff

added theorem finset.attach_nonempty_iff

added theorem finset.eq_empty_of_ssubset_singleton

added theorem finset.exists_of_ssubset

added theorem finset.ssubset_of_ssubset_of_subset

added theorem finset.ssubset_of_subset_of_ssubset

added theorem finset.ssubset_singleton_iff

added theorem finset.subset_inter_iff

added theorem finset.subset_singleton_iff

added theorem finset.union_subset_iff

modified theorem finset.union_subset_union

Modified src/data/set/basic.lean

added theorem set.diff_union_of_subset

added theorem set.eq_empty_of_ssubset_singleton

added theorem set.ssubset_of_ssubset_of_subset

added theorem set.ssubset_of_subset_of_ssubset

added theorem set.ssubset_singleton_iff

added theorem set.subset_singleton_iff_eq