mathlib documentation

data.finset.powerset

The powerset of a finset #

powerset #

def finset.powerset {α : Type u_1} (s : finset α) :

When s is a finset, s.powerset is the finset of all subsets of s (seen as finsets).

Equations
@[simp]
theorem finset.mem_powerset {α : Type u_1} {s t : finset α} :
@[simp]
theorem finset.empty_mem_powerset {α : Type u_1} (s : finset α) :
@[simp]
theorem finset.mem_powerset_self {α : Type u_1} (s : finset α) :
@[simp]
theorem finset.powerset_empty {α : Type u_1} :
@[simp]
theorem finset.powerset_mono {α : Type u_1} {s t : finset α} :
@[simp]
theorem finset.card_powerset {α : Type u_1} (s : finset α) :

Number of Subsets of a Set

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
theorem finset.powerset_insert {α : Type u_1} [decidable_eq α] (s : finset α) (a : α) :
@[protected, instance]
def finset.decidable_exists_of_decidable_subsets {α : Type u_1} {s : finset α} {p : Π (t : finset α), t s → Prop} [Π (t : finset α) (h : t s), decidable (p t h)] :
decidable (∃ (t : finset α) (h : t s), p t h)

For predicate p decidable on subsets, it is decidable whether p holds for any subset.

Equations
@[protected, instance]
def finset.decidable_forall_of_decidable_subsets {α : Type u_1} {s : finset α} {p : Π (t : finset α), t s → Prop} [Π (t : finset α) (h : t s), decidable (p t h)] :
decidable (∀ (t : finset α) (h : t s), p t h)

For predicate p decidable on subsets, it is decidable whether p holds for every subset.

Equations
def finset.decidable_exists_of_decidable_subsets' {α : Type u_1} {s : finset α} {p : finset α → Prop} (hu : Π (t : finset α), t sdecidable (p t)) :
decidable (∃ (t : finset α) (h : t s), p t)

A version of finset.decidable_exists_of_decidable_subsets with a non-dependent p. Typeclass inference cannot find hu here, so this is not an instance.

Equations
def finset.decidable_forall_of_decidable_subsets' {α : Type u_1} {s : finset α} {p : finset α → Prop} (hu : Π (t : finset α), t sdecidable (p t)) :
decidable (∀ (t : finset α), t sp t)

A version of finset.decidable_forall_of_decidable_subsets with a non-dependent p. Typeclass inference cannot find hu here, so this is not an instance.

Equations
def finset.ssubsets {α : Type u_1} [decidable_eq α] (s : finset α) :

For s a finset, s.ssubsets is the finset comprising strict subsets of s.

Equations
@[simp]
theorem finset.mem_ssubsets {α : Type u_1} [decidable_eq α] {s t : finset α} :
theorem finset.empty_mem_ssubsets {α : Type u_1} [decidable_eq α] {s : finset α} (h : s.nonempty) :
@[protected, instance]
def finset.decidable_exists_of_decidable_ssubsets {α : Type u_1} [decidable_eq α] {s : finset α} {p : Π (t : finset α), t s → Prop} [Π (t : finset α) (h : t s), decidable (p t h)] :
decidable (∃ (t : finset α) (h : t s), p t h)

For predicate p decidable on ssubsets, it is decidable whether p holds for any ssubset.

Equations
@[protected, instance]
def finset.decidable_forall_of_decidable_ssubsets {α : Type u_1} [decidable_eq α] {s : finset α} {p : Π (t : finset α), t s → Prop} [Π (t : finset α) (h : t s), decidable (p t h)] :
decidable (∀ (t : finset α) (h : t s), p t h)

For predicate p decidable on ssubsets, it is decidable whether p holds for every ssubset.

Equations
def finset.decidable_exists_of_decidable_ssubsets' {α : Type u_1} [decidable_eq α] {s : finset α} {p : finset α → Prop} (hu : Π (t : finset α), t sdecidable (p t)) :
decidable (∃ (t : finset α) (h : t s), p t)

A version of finset.decidable_exists_of_decidable_ssubsets with a non-dependent p. Typeclass inference cannot find hu here, so this is not an instance.

Equations
def finset.decidable_forall_of_decidable_ssubsets' {α : Type u_1} [decidable_eq α] {s : finset α} {p : finset α → Prop} (hu : Π (t : finset α), t sdecidable (p t)) :
decidable (∀ (t : finset α), t sp t)

A version of finset.decidable_forall_of_decidable_ssubsets with a non-dependent p. Typeclass inference cannot find hu here, so this is not an instance.

Equations
def finset.powerset_len {α : Type u_1} (n : ) (s : finset α) :

Given an integer n and a finset s, then powerset_len n s is the finset of subsets of s of cardinality n.

Equations
theorem finset.mem_powerset_len {α : Type u_1} {n : } {s t : finset α} :

Formula for the Number of Combinations

@[simp]
theorem finset.powerset_len_mono {α : Type u_1} {n : } {s t : finset α} (h : s t) :
@[simp]
theorem finset.card_powerset_len {α : Type u_1} (n : ) (s : finset α) :

Formula for the Number of Combinations

@[simp]
theorem finset.powerset_len_zero {α : Type u_1} (s : finset α) :
@[simp]
theorem finset.powerset_len_empty {α : Type u_1} (n : ) {s : finset α} (h : s.card < n) :
theorem finset.powerset_len_eq_filter {α : Type u_1} {n : } {s : finset α} :
theorem finset.powerset_len_succ_insert {α : Type u_1} [decidable_eq α] {x : α} {s : finset α} (h : x s) (n : ) :
theorem finset.powerset_len_nonempty {α : Type u_1} {n : } {s : finset α} (h : n < s.card) :
@[simp]
theorem finset.powerset_len_self {α : Type u_1} (s : finset α) :
theorem finset.powerset_card_bUnion {α : Type u_1} [decidable_eq (finset α)] (s : finset α) :
theorem finset.powerset_len_sup {α : Type u_1} [decidable_eq α] (u : finset α) (n : ) (hn : n < u.card) :
@[simp]
theorem finset.powerset_len_card_add {α : Type u_1} (s : finset α) {i : } (hi : 0 < i) :