Documentation

Mathlib.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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Finset.mem_powerset {α : Type u_1} {s : Finset α} {t : Finset α} :
@[simp]
theorem Finset.coe_powerset {α : Type u_1} (s : Finset α) :
↑(Finset.powerset s) = Finset.toSet ⁻¹' 𝒫s
@[simp]
theorem Finset.powerset_mono {α : Type u_1} {s : Finset α} {t : Finset α} :
theorem Finset.powerset_injective {α : Type u_1} :
Function.Injective Finset.powerset
@[simp]
theorem Finset.powerset_inj {α : Type u_1} {s : Finset α} {t : Finset α} :
@[simp]

Number of Subsets of a Set

theorem Finset.not_mem_of_mem_powerset_of_not_mem {α : Type u_1} {s : Finset α} {t : Finset α} {a : α} (ht : t Finset.powerset s) (h : ¬a s) :
¬a t
instance Finset.decidableExistsOfDecidableSubsets {α : Type u_1} {s : Finset α} {p : (t : Finset α) → t sProp} [inst : (t : Finset α) → (h : t s) → Decidable (p t h)] :
Decidable (t h, p t h)

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

Equations
  • Finset.decidableExistsOfDecidableSubsets = decidable_of_iff (t hs, p t (_ : t s)) (_ : (t hs, p t (_ : t s)) t h, p t h)
instance Finset.decidableForallOfDecidableSubsets {α : Type u_1} {s : Finset α} {p : (t : Finset α) → t sProp} [inst : (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
  • One or more equations did not get rendered due to their size.
def Finset.decidableExistsOfDecidableSubsets' {α : Type u_1} {s : Finset α} {p : Finset αProp} (hu : (t : Finset α) → t sDecidable (p t)) :
Decidable (t _h, p t)

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

Equations
def Finset.decidableForallOfDecidableSubsets' {α : 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.decidableForallOfDecidableSubsets with a non-dependent p. Typeclass inference cannot find hu here, so this is not an instance.

Equations
def Finset.ssubsets {α : Type u_1} [inst : DecidableEq α] (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} [inst : DecidableEq α] {s : Finset α} {t : Finset α} :
instance Finset.decidableExistsOfDecidableSsubsets {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {p : (t : Finset α) → t sProp} [inst : (t : Finset α) → (h : t s) → Decidable (p t h)] :
Decidable (t h, p t h)

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

Equations
  • Finset.decidableExistsOfDecidableSsubsets = decidable_of_iff (t hs, p t (_ : t s)) (_ : (t hs, p t (_ : t s)) t h, p t h)
instance Finset.decidableForallOfDecidableSsubsets {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {p : (t : Finset α) → t sProp} [inst : (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
  • One or more equations did not get rendered due to their size.
def Finset.decidableExistsOfDecidableSsubsets' {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {p : Finset αProp} (hu : (t : Finset α) → t sDecidable (p t)) :
Decidable (t _h, 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
def Finset.decidableForallOfDecidableSsubsets' {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {p : Finset αProp} (hu : (t : Finset α) → t sDecidable (p t)) :
Decidable ((t : Finset α) → t sp t)

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

Equations
def Finset.powersetLen {α : Type u_1} (n : ) (s : Finset α) :

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

Equations
  • One or more equations did not get rendered due to their size.
theorem Finset.mem_powersetLen {α : Type u_1} {n : } {s : Finset α} {t : Finset α} :

Formula for the Number of Combinations

@[simp]
theorem Finset.powersetLen_mono {α : Type u_1} {n : } {s : Finset α} {t : Finset α} (h : s t) :
@[simp]

Formula for the Number of Combinations

@[simp]
theorem Finset.powersetLen_zero {α : Type u_1} (s : Finset α) :
@[simp]
theorem Finset.powersetLen_empty {α : Type u_1} (n : ) {s : Finset α} (h : Finset.card s < n) :
@[simp]
theorem Finset.powersetLen_self {α : Type u_1} (s : Finset α) :
theorem Finset.powerset_len_sup {α : Type u_1} [inst : DecidableEq α] (u : Finset α) (n : ) (hn : n < Finset.card u) :
@[simp]
theorem Finset.powersetLen_card_add {α : Type u_1} (s : Finset α) {i : } (hi : 0 < i) :
@[simp]
theorem Finset.map_val_val_powersetLen {α : Type u_1} (s : Finset α) (i : ) :
theorem Finset.powersetLen_map {α : Type u_2} {β : Type u_1} (f : α β) (n : ) (s : Finset α) :