Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-31 21:08 ca740b64

View on Github →

feat(data/finset/powerset): ssubsets and decidability (#7543) A few more little additions to finset-world that I found useful.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.ssubset_iff_subset_ne

Modified src/data/finset/powerset.lean

added def finset.decidable_exists_of_decidable_ssubsets'

added def finset.decidable_exists_of_decidable_subsets'

added def finset.decidable_forall_of_decidable_ssubsets'

added def finset.decidable_forall_of_decidable_subsets'

added theorem finset.empty_mem_ssubsets

added theorem finset.mem_ssubsets

added def finset.ssubsets