The powerset of a finset #
powerset #
Number of Subsets of a Set
A version of Finset.decidableExistsOfDecidableSubsets
with a non-dependent p
.
Typeclass inference cannot find hu
here, so this is not an instance.
Instances For
A version of Finset.decidableForallOfDecidableSubsets
with a non-dependent p
.
Typeclass inference cannot find hu
here, so this is not an instance.
Instances For
For s
a finset, s.ssubsets
is the finset comprising strict subsets of s
.
Instances For
For predicate p
decidable on ssubsets, it is decidable whether p
holds for every ssubset.
A version of Finset.decidableExistsOfDecidableSSubsets
with a non-dependent p
.
Typeclass inference cannot find hu
here, so this is not an instance.
Instances For
A version of Finset.decidableForallOfDecidableSSubsets
with a non-dependent p
.
Typeclass inference cannot find hu
here, so this is not an instance.
Instances For
Given an integer n
and a finset s
, then powersetLen n s
is the finset of subsets of s
of cardinality n
.
Instances For
Formula for the Number of Combinations
Formula for the Number of Combinations