mathlib documentation

data.finset.powerset

The powerset of a finset

powerset

def finset.powerset {α : Type u_1} :
finset αfinset (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 : α} :
t s.powerseta sa t

theorem finset.powerset_insert {α : Type u_1} [decidable_eq α] (s : finset α) (a : α) :

def finset.powerset_len {α : Type u_1} :
finset αfinset (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 α} :

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