The powerset of a finset #
powerset #
@[deprecated Finset.notMem_of_mem_powerset_of_notMem (since := "2025-05-23")]
theorem
Finset.not_mem_of_mem_powerset_of_not_mem
{α : Type u_1}
{s t : Finset α}
{a : α}
(ht : t ∈ s.powerset)
(h : a ∉ s)
:
a ∉ t
Alias of Finset.notMem_of_mem_powerset_of_notMem
.
theorem
Finset.pairwiseDisjoint_pair_insert
{α : Type u_1}
{s : Finset α}
[DecidableEq α]
{a : α}
(ha : a ∉ s)
:
@[simp]
def
Finset.decidableExistsOfDecidableSSubsets
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
{p : (t : Finset α) → t ⊂ s → Prop}
[(t : Finset α) → (h : t ⊂ s) → Decidable (p t h)]
:
For predicate p
decidable on ssubsets, it is decidable whether p
holds for any ssubset.
Equations
Instances For
def
Finset.decidableForallOfDecidableSSubsets
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
{p : (t : Finset α) → t ⊂ s → Prop}
[(t : Finset α) → (h : t ⊂ s) → Decidable (p t h)]
:
For predicate p
decidable on ssubsets, it is decidable whether p
holds for every ssubset.
Equations
Instances For
def
Finset.decidableExistsOfDecidableSSubsets'
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
{p : Finset α → Prop}
(hu : (t : Finset α) → t ⊂ s → Decidable (p t))
:
A version of Finset.decidableExistsOfDecidableSSubsets
with a non-dependent p
.
Typeclass inference cannot find hu
here, so this is not an instance.
Equations
Instances For
def
Finset.decidableForallOfDecidableSSubsets'
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
{p : Finset α → Prop}
(hu : (t : Finset α) → t ⊂ s → Decidable (p t))
:
Decidable (∀ t ⊂ s, p t)
A version of Finset.decidableForallOfDecidableSSubsets
with a non-dependent p
.
Typeclass inference cannot find hu
here, so this is not an instance.
Equations
Instances For
Given an integer n
and a finset s
, then powersetCard n s
is the finset of subsets of s
of cardinality n
.
Equations
Instances For
@[simp]
@[simp]
Formula for the Number of Combinations
@[simp]
theorem
Finset.powersetCard_empty_subsingleton
{α : Type u_1}
(n : ℕ)
:
(↑(powersetCard n ∅)).Subsingleton
@[simp]
theorem
Finset.powersetCard_succ_insert
{α : Type u_1}
[DecidableEq α]
{x : α}
{s : Finset α}
(h : x ∉ s)
(n : ℕ)
:
@[simp]
theorem
Finset.powersetCard_nonempty_of_le
{α : Type u_1}
{n : ℕ}
{s : Finset α}
:
n ≤ s.card → (powersetCard n s).Nonempty
Alias of the reverse direction of Finset.powersetCard_nonempty
.
@[simp]
theorem
Finset.pairwise_disjoint_powersetCard
{α : Type u_1}
(s : Finset α)
:
Pairwise fun (i j : ℕ) => Disjoint (powersetCard i s) (powersetCard j s)
theorem
Finset.powersetCard_sup
{α : Type u_1}
[DecidableEq α]
(u : Finset α)
(n : ℕ)
(hn : n < u.card)
: