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 α) :
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 : α) :
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 α} :
@[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 α) :
@[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) :