Mathlib.Data.Finset.Powerset

Finset.powerset definition

(s : Finset α) : Finset (Finset α)

Full source

/-- When `s` is a finset, `s.powerset` is the finset of all subsets of `s` (seen as finsets). -/
def powerset (s : Finset α) : Finset (Finset α) :=
  ⟨(s.1.powerset.pmap Finset.mk) fun _t h => nodup_of_le (mem_powerset.1 h) s.nodup,
    s.nodup.powerset.pmap fun _a _ha _b _hb => congr_arg Finset.val⟩

Power set of a finite set

Informal description

Given a finite set $ s $ of type $ \alpha $, the function `Finset.powerset` returns the finite set consisting of all subsets of $ s $, where each subset is also represented as a finite set.

Finset.mem_powerset theorem

{s t : Finset α} : s ∈ powerset t ↔ s ⊆ t

Full source

@[simp]
theorem mem_powerset {s t : Finset α} : s ∈ powerset ts ∈ powerset t ↔ s ⊆ t := by
  cases s
  simp [powerset, mem_mk, mem_pmap, mk.injEq, mem_powerset, exists_prop, exists_eq_right,
    ← val_le_iff]

Membership in Powerset Characterized by Subset Relation

Informal description

For any finite sets $s$ and $t$ of type $\alpha$, $s$ is an element of the power set of $t$ if and only if $s$ is a subset of $t$, i.e., $s \in \mathcal{P}(t) \leftrightarrow s \subseteq t$.

Finset.coe_powerset theorem

(s : Finset α) : (s.powerset : Set (Finset α)) = ((↑) : Finset α → Set α) ⁻¹' (s : Set α).powerset

Full source

@[simp, norm_cast]
theorem coe_powerset (s : Finset α) :
    (s.powerset : Set (Finset α)) = ((↑) : Finset α → Set α) ⁻¹' (s : Set α).powerset := by
  ext
  simp

Coercion of Finite Powerset Equals Preimage of Set Powerset

Informal description

For any finite set $s$ of type $\alpha$, the image of the powerset of $s$ under the coercion from `Finset α` to `Set α` is equal to the preimage of the powerset of $s$ (viewed as a set) under the same coercion. In other words, $(s.\text{powerset} : \text{Set} (\text{Finset} \alpha)) = (\uparrow)^{-1} (s : \text{Set} \alpha).\text{powerset}$. Here, $\uparrow$ denotes the canonical embedding from finite sets to sets, and $\text{powerset}$ denotes the collection of all subsets.

Finset.empty_mem_powerset theorem

(s : Finset α) : ∅ ∈ powerset s

Full source

theorem empty_mem_powerset (s : Finset α) : ∅∅ ∈ powerset s := by simp

Empty Set Belongs to Powerset of Any Finite Set

Informal description

For any finite set $s$ of type $\alpha$, the empty set $\emptyset$ is an element of the powerset of $s$.

Finset.mem_powerset_self theorem

(s : Finset α) : s ∈ powerset s

Full source

theorem mem_powerset_self (s : Finset α) : s ∈ powerset s := by simp

Self-Membership in Powerset of Finite Set

Informal description

For any finite set $s$ of type $\alpha$, the set $s$ is an element of its own powerset, i.e., $s \in \mathcal{P}(s)$.

Finset.powerset_nonempty theorem

(s : Finset α) : s.powerset.Nonempty

Full source

@[aesop safe apply (rule_sets := [finsetNonempty])]
theorem powerset_nonempty (s : Finset α) : s.powerset.Nonempty :=
  ⟨∅, empty_mem_powerset _⟩

Nonempty Powerset of a Finite Set

Informal description

For any finite set $s$ of type $\alpha$, the powerset of $s$ is nonempty.

Finset.powerset_mono theorem

{s t : Finset α} : powerset s ⊆ powerset t ↔ s ⊆ t

Full source

@[simp]
theorem powerset_mono {s t : Finset α} : powersetpowerset s ⊆ powerset tpowerset s ⊆ powerset t ↔ s ⊆ t :=
  ⟨fun h => mem_powerset.1 <| h <| mem_powerset_self _, fun st _u h =>
    mem_powerset.2 <| Subset.trans (mem_powerset.1 h) st⟩

Powerset Monotonicity: $\mathcal{P}(s) \subseteq \mathcal{P}(t) \leftrightarrow s \subseteq t$

Informal description

For any finite sets $s$ and $t$ of type $\alpha$, the powerset of $s$ is a subset of the powerset of $t$ if and only if $s$ is a subset of $t$, i.e., $\mathcal{P}(s) \subseteq \mathcal{P}(t) \leftrightarrow s \subseteq t$.

Finset.powerset_injective theorem

: Injective (powerset : Finset α → Finset (Finset α))

Full source

theorem powerset_injective : Injective (powerset : Finset α → Finset (Finset α)) :=
  (injective_of_le_imp_le _) powerset_mono.1

Injectivity of the Powerset Function on Finite Sets

Informal description

The powerset function $\mathcal{P} : \text{Finset } \alpha \to \text{Finset } (\text{Finset } \alpha)$, which maps a finite set $s$ to the finite set of all its subsets, is injective. That is, for any finite sets $s$ and $t$ of type $\alpha$, if $\mathcal{P}(s) = \mathcal{P}(t)$, then $s = t$.

Finset.powerset_inj theorem

: powerset s = powerset t ↔ s = t

Full source

@[simp]
theorem powerset_inj : powersetpowerset s = powerset t ↔ s = t :=
  powerset_injective.eq_iff

Powerset Equality Criterion for Finite Sets: $\mathcal{P}(s) = \mathcal{P}(t) \leftrightarrow s = t$

Informal description

For any finite sets $s$ and $t$ of type $\alpha$, the powerset of $s$ equals the powerset of $t$ if and only if $s = t$.

Finset.powerset_empty theorem

: (∅ : Finset α).powerset = {∅}

Full source

@[simp]
theorem powerset_empty : (∅ : Finset α).powerset = {∅} :=
  rfl

Power Set of Empty Finite Set is Singleton of Empty Set

Informal description

The power set of the empty finite set is the singleton set containing only the empty set, i.e., $\mathcal{P}(\emptyset) = \{\emptyset\}$.

Finset.powerset_eq_singleton_empty theorem

: s.powerset = {∅} ↔ s = ∅

Full source

@[simp]
theorem powerset_eq_singleton_empty : s.powerset = {∅} ↔ s = ∅ := by
  rw [← powerset_empty, powerset_inj]

Power Set is Singleton of Empty Set iff Set is Empty: $\mathcal{P}(s) = \{\emptyset\} \leftrightarrow s = \emptyset$

Informal description

For any finite set $s$ of type $\alpha$, the power set of $s$ is equal to the singleton set $\{\emptyset\}$ if and only if $s$ is the empty set. In other words, $\mathcal{P}(s) = \{\emptyset\} \leftrightarrow s = \emptyset$.

Finset.card_powerset theorem

(s : Finset α) : card (powerset s) = 2 ^ card s

Full source

/-- **Number of Subsets of a Set** -/
@[simp]
theorem card_powerset (s : Finset α) : card (powerset s) = 2 ^ card s :=
  (card_pmap _ _ _).trans (Multiset.card_powerset s.1)

Cardinality of Power Set of a Finite Set: $|\mathcal{P}(s)| = 2^{|s|}$

Informal description

For any finite set $s$ of type $\alpha$, the cardinality of its power set $\mathcal{P}(s)$ is equal to $2$ raised to the power of the cardinality of $s$, i.e., $$|\mathcal{P}(s)| = 2^{|s|}.$$

Finset.not_mem_of_mem_powerset_of_not_mem theorem

{s t : Finset α} {a : α} (ht : t ∈ s.powerset) (h : a ∉ s) : a ∉ t

Full source

theorem not_mem_of_mem_powerset_of_not_mem {s t : Finset α} {a : α} (ht : t ∈ s.powerset)
    (h : a ∉ s) : a ∉ t := by
  apply mt _ h
  apply mem_powerset.1 ht

Element Exclusion in Subsets: $a \notin s \implies a \notin t$ for $t \subseteq s$

Informal description

For any finite sets $s$ and $t$ of a type $\alpha$, and any element $a \in \alpha$, if $t$ is a subset of $s$ (i.e., $t \in \mathcal{P}(s)$) and $a$ is not an element of $s$, then $a$ is not an element of $t$.

Finset.powerset_insert theorem

[DecidableEq α] (s : Finset α) (a : α) : powerset (insert a s) = s.powerset ∪ s.powerset.image (insert a)

Full source

theorem powerset_insert [DecidableEq α] (s : Finset α) (a : α) :
    powerset (insert a s) = s.powerset ∪ s.powerset.image (insert a) := by
  ext t
  simp only [exists_prop, mem_powerset, mem_image, mem_union, subset_insert_iff]
  by_cases h : a ∈ t
  · constructor
    · exact fun H => Or.inr ⟨_, H, insert_erase h⟩
    · intro H
      rcases H with H | H
      · exact Subset.trans (erase_subset a t) H
      · rcases H with ⟨u, hu⟩
        rw [← hu.2]
        exact Subset.trans (erase_insert_subset a u) hu.1
  · have : ¬∃ u : Finset α, u ⊆ s ∧ insert a u = t := by simp [Ne.symm (ne_insert_of_not_mem _ _ h)]
    simp [Finset.erase_eq_of_not_mem h, this]

Power Set of Insertion Equals Union of Power Set and Its Inserted Image

Informal description

For any finite set $s$ of type $\alpha$ with decidable equality and any element $a \in \alpha$, the power set of $s \cup \{a\}$ is equal to the union of the power set of $s$ and the image of the power set of $s$ under the operation of inserting $a$ into each subset. In other words, \[ \mathcal{P}(s \cup \{a\}) = \mathcal{P}(s) \cup \{ t \cup \{a\} \mid t \in \mathcal{P}(s) \}. \]

Finset.pairwiseDisjoint_pair_insert theorem

 [DecidableEq α] {a : α} (ha : a ∉ s) :
  (s.powerset : Set (Finset α)).PairwiseDisjoint fun t ↦ ({t, insert a t} : Set (Finset α))

Full source

lemma pairwiseDisjoint_pair_insert [DecidableEq α] {a : α} (ha : a ∉ s) :
    (s.powerset : Set (Finset α)).PairwiseDisjoint fun t ↦ ({t, insert a t} : Set (Finset α)) := by
  simp_rw [Set.pairwiseDisjoint_iff, mem_coe, mem_powerset]
  rintro i hi j hj
  simp only [Set.Nonempty, Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
    exists_eq_or_imp, exists_eq_left, or_imp, imp_self, true_and]
  refine ⟨?_, ?_, insert_erase_invOn.2.injOn (not_mem_mono hi ha) (not_mem_mono hj ha)⟩ <;>
    rintro rfl <;>
    cases Finset.not_mem_mono ‹_› ha (Finset.mem_insert_self _ _)

Pairwise Disjointness of Insertion Pairs in Power Set

Informal description

For a finite set $s$ of type $\alpha$ with decidable equality and an element $a \notin s$, the family of sets $\{\{t, t \cup \{a\}\} \mid t \in \mathcal{P}(s)\}$ is pairwise disjoint, where $\mathcal{P}(s)$ denotes the power set of $s$.

Finset.decidableExistsOfDecidableSubsets instance

 {s : Finset α} {p : ∀ t ⊆ s, Prop} [∀ (t) (h : t ⊆ s), Decidable (p t h)] : Decidable (∃ (t : _) (h : t ⊆ s), p t h)

Full source

/-- For predicate `p` decidable on subsets, it is decidable whether `p` holds for any subset. -/
instance decidableExistsOfDecidableSubsets {s : Finset α} {p : ∀ t ⊆ s, Prop}
    [∀ (t) (h : t ⊆ s), Decidable (p t h)] : Decidable (∃ (t : _) (h : t ⊆ s), p t h) :=
  decidable_of_iff (∃ (t : _) (hs : t ∈ s.powerset), p t (mem_powerset.1 hs))
    ⟨fun ⟨t, _, hp⟩ => ⟨t, _, hp⟩, fun ⟨t, hs, hp⟩ => ⟨t, mem_powerset.2 hs, hp⟩⟩

Decidability of Existential Quantification over Subsets of a Finite Set

Informal description

For any finite set $s$ of type $\alpha$ and any predicate $p$ defined for subsets $t \subseteq s$ with decidable values, it is decidable whether there exists a subset $t \subseteq s$ such that $p(t)$ holds.

Finset.decidableForallOfDecidableSubsets instance

 {s : Finset α} {p : ∀ t ⊆ s, Prop} [∀ (t) (h : t ⊆ s), Decidable (p t h)] : Decidable (∀ (t) (h : t ⊆ s), p t h)

Full source

/-- For predicate `p` decidable on subsets, it is decidable whether `p` holds for every subset. -/
instance decidableForallOfDecidableSubsets {s : Finset α} {p : ∀ t ⊆ s, Prop}
    [∀ (t) (h : t ⊆ s), Decidable (p t h)] : Decidable (∀ (t) (h : t ⊆ s), p t h) :=
  decidable_of_iff (∀ (t) (h : t ∈ s.powerset), p t (mem_powerset.1 h))
    ⟨fun h t hs => h t (mem_powerset.2 hs), fun h _ _ => h _ _⟩

Decidability of Universal Quantification over Subsets of a Finite Set

Informal description

For any finite set $s$ of type $\alpha$ and any predicate $p$ defined for subsets $t \subseteq s$ with decidable values, it is decidable whether for all subsets $t \subseteq s$, $p(t)$ holds.

Finset.decidableExistsOfDecidableSubsets' instance

{s : Finset α} {p : Finset α → Prop} [∀ t, Decidable (p t)] : Decidable (∃ t ⊆ s, p t)

Full source

/-- For predicate `p` decidable on subsets, it is decidable whether `p` holds for any subset. -/
instance decidableExistsOfDecidableSubsets' {s : Finset α} {p : Finset α → Prop}
    [∀ t, Decidable (p t)] : Decidable (∃ t ⊆ s, p t) :=
  decidable_of_iff (∃ (t : _) (_h : t ⊆ s), p t) <| by simp

Decidability of Existential Quantification over Subsets of a Finite Set

Informal description

For any finite set $s$ of type $\alpha$ and any predicate $p$ on finite subsets of $\alpha$ with decidable values, it is decidable whether there exists a subset $t \subseteq s$ such that $p(t)$ holds.

Finset.decidableForallOfDecidableSubsets' instance

{s : Finset α} {p : Finset α → Prop} [∀ t, Decidable (p t)] : Decidable (∀ t ⊆ s, p t)

Full source

/-- For predicate `p` decidable on subsets, it is decidable whether `p` holds for every subset. -/
instance decidableForallOfDecidableSubsets' {s : Finset α} {p : Finset α → Prop}
    [∀ t, Decidable (p t)] : Decidable (∀ t ⊆ s, p t) :=
  decidable_of_iff (∀ (t : _) (_h : t ⊆ s), p t) <| by simp

Decidability of Universal Quantification over Subsets of a Finite Set

Informal description

For any finite set $s$ of type $\alpha$ and any predicate $p$ defined on finite subsets of $\alpha$ with decidable values, it is decidable whether for all subsets $t \subseteq s$, $p(t)$ holds.

Finset.ssubsets definition

(s : Finset α) : Finset (Finset α)

Full source

/-- For `s` a finset, `s.ssubsets` is the finset comprising strict subsets of `s`. -/
def ssubsets (s : Finset α) : Finset (Finset α) :=
  erase (powerset s) s

Strict subsets of a finite set

Informal description

For a finite set $ s $ of type $ \alpha $, the function `Finset.ssubsets` returns the finite set consisting of all strict subsets of $ s $, where each subset is also represented as a finite set. A strict subset $ t $ satisfies $ t \subset s $.

Finset.mem_ssubsets theorem

{s t : Finset α} : t ∈ s.ssubsets ↔ t ⊂ s

Full source

@[simp]
theorem mem_ssubsets {s t : Finset α} : t ∈ s.ssubsetst ∈ s.ssubsets ↔ t ⊂ s := by
  rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]

Characterization of Membership in Strict Subsets: $t \in \text{ssubsets}(s) \leftrightarrow t \subset s$

Informal description

For any finite sets $s$ and $t$ of type $\alpha$, $t$ is an element of the set of strict subsets of $s$ if and only if $t$ is a strict subset of $s$, i.e., $t \in \text{ssubsets}(s) \leftrightarrow t \subset s$.

Finset.empty_mem_ssubsets theorem

{s : Finset α} (h : s.Nonempty) : ∅ ∈ s.ssubsets

Full source

theorem empty_mem_ssubsets {s : Finset α} (h : s.Nonempty) : ∅∅ ∈ s.ssubsets := by
  rw [mem_ssubsets, ssubset_iff_subset_ne]
  exact ⟨empty_subset s, h.ne_empty.symm⟩

Empty Set is a Strict Subset of Any Nonempty Finite Set

Informal description

For any nonempty finite set $s$ of type $\alpha$, the empty set $\emptyset$ is a strict subset of $s$, i.e., $\emptyset \in \text{ssubsets}(s)$.

Finset.decidableExistsOfDecidableSSubsets definition

{s : Finset α} {p : ∀ t ⊂ s, Prop} [∀ t h, Decidable (p t h)] : Decidable (∃ t h, p t h)

Full source

/-- For predicate `p` decidable on ssubsets, it is decidable whether `p` holds for any ssubset. -/
def decidableExistsOfDecidableSSubsets {s : Finset α} {p : ∀ t ⊂ s, Prop}
    [∀ t h, Decidable (p t h)] : Decidable (∃ t h, p t h) :=
  decidable_of_iff (∃ (t : _) (hs : t ∈ s.ssubsets), p t (mem_ssubsets.1 hs))
    ⟨fun ⟨t, _, hp⟩ => ⟨t, _, hp⟩, fun ⟨t, hs, hp⟩ => ⟨t, mem_ssubsets.2 hs, hp⟩⟩

Decidability of existential quantification over strict subsets of a finite set

Informal description

For a finite set $ s $ of type $ \alpha $ and a predicate $ p $ defined for all strict subsets $ t \subset s $ with decidable values, it is decidable whether there exists a strict subset $ t \subset s $ such that $ p(t) $ holds.

Finset.decidableForallOfDecidableSSubsets definition

{s : Finset α} {p : ∀ t ⊂ s, Prop} [∀ t h, Decidable (p t h)] : Decidable (∀ t h, p t h)

Full source

/-- For predicate `p` decidable on ssubsets, it is decidable whether `p` holds for every ssubset. -/
def decidableForallOfDecidableSSubsets {s : Finset α} {p : ∀ t ⊂ s, Prop}
    [∀ t h, Decidable (p t h)] : Decidable (∀ t h, p t h) :=
  decidable_of_iff (∀ (t) (h : t ∈ s.ssubsets), p t (mem_ssubsets.1 h))
    ⟨fun h t hs => h t (mem_ssubsets.2 hs), fun h _ _ => h _ _⟩

Decidability of universal quantification over strict subsets of a finite set

Informal description

For a finite set $ s $ of type $ \alpha $ and a predicate $ p $ on strict subsets of $ s $ (where $ p $ is decidable for each strict subset), the universal quantification $ \forall t \subset s, p(t) $ is decidable.

Finset.decidableExistsOfDecidableSSubsets' definition

 {s : Finset α} {p : Finset α → Prop} (hu : ∀ t ⊂ s, Decidable (p t)) : Decidable (∃ (t : _) (_h : t ⊂ s), p t)

Full source

/-- A version of `Finset.decidableExistsOfDecidableSSubsets` with a non-dependent `p`.
Typeclass inference cannot find `hu` here, so this is not an instance. -/
def decidableExistsOfDecidableSSubsets' {s : Finset α} {p : Finset α → Prop}
    (hu : ∀ t ⊂ s, Decidable (p t)) : Decidable (∃ (t : _) (_h : t ⊂ s), p t) :=
  @Finset.decidableExistsOfDecidableSSubsets _ _ _ _ hu

Decidability of existential quantification over strict subsets of a finite set (non-dependent version)

Informal description

For a finite set $ s $ of type $ \alpha $ and a predicate $ p $ on subsets of $ s $ (where $ p $ is decidable for each strict subset $ t \subset s $), it is decidable whether there exists a strict subset $ t \subset s $ such that $ p(t) $ holds.

Finset.decidableForallOfDecidableSSubsets' definition

{s : Finset α} {p : Finset α → Prop} (hu : ∀ t ⊂ s, Decidable (p t)) : Decidable (∀ t ⊂ s, p t)

Full source

/-- A version of `Finset.decidableForallOfDecidableSSubsets` with a non-dependent `p`.
Typeclass inference cannot find `hu` here, so this is not an instance. -/
def decidableForallOfDecidableSSubsets' {s : Finset α} {p : Finset α → Prop}
    (hu : ∀ t ⊂ s, Decidable (p t)) : Decidable (∀ t ⊂ s, p t) :=
  @Finset.decidableForallOfDecidableSSubsets _ _ _ _ hu

Decidability of universal quantification over strict subsets of a finite set (non-dependent version)

Informal description

For a finite set $ s $ of type $ \alpha $ and a predicate $ p $ on finite subsets of $ \alpha $ (where $ p $ is decidable for each strict subset $ t \subset s $), the universal quantification $ \forall t \subset s, p(t) $ is decidable.

Finset.powersetCard definition

(n : ℕ) (s : Finset α) : Finset (Finset α)

Full source

/-- Given an integer `n` and a finset `s`, then `powersetCard n s` is the finset of subsets of `s`
of cardinality `n`. -/
def powersetCard (n : ℕ) (s : Finset α) : Finset (Finset α) :=
  ⟨((s.1.powersetCard n).pmap Finset.mk) fun _t h => nodup_of_le (mem_powersetCard.1 h).1 s.2,
    s.2.powersetCard.pmap fun _a _ha _b _hb => congr_arg Finset.val⟩

Finite set of subsets with fixed cardinality

Informal description

For a natural number $ n $ and a finite set $ s $ of elements of type $ \alpha $, the function `powersetCard` returns the finite set of all subsets of $ s $ with exactly $ n $ elements. More precisely, a subset $ t $ is in `powersetCard n s` if and only if $ t $ is a subset of $ s $ (i.e., $ t \subseteq s $) and the cardinality of $ t $ is $ n $.

Finset.mem_powersetCard theorem

: s ∈ powersetCard n t ↔ s ⊆ t ∧ card s = n

Full source

@[simp] lemma mem_powersetCard : s ∈ powersetCard n ts ∈ powersetCard n t ↔ s ⊆ t ∧ card s = n := by
  cases s; simp [powersetCard, val_le_iff.symm]

Characterization of Fixed-Size Subsets: $s \in \text{powersetCard}_n(t) \leftrightarrow s \subseteq t \land |s| = n$

Informal description

For any finite set $t$ of type $\alpha$ and natural number $n$, a finite set $s$ is an element of $\text{powersetCard}_n(t)$ if and only if $s$ is a subset of $t$ and the cardinality of $s$ is equal to $n$. In other words: $$ s \in \text{powersetCard}_n(t) \leftrightarrow s \subseteq t \land |s| = n $$

Finset.powersetCard_mono theorem

{n} {s t : Finset α} (h : s ⊆ t) : powersetCard n s ⊆ powersetCard n t

Full source

@[simp]
theorem powersetCard_mono {n} {s t : Finset α} (h : s ⊆ t) : powersetCardpowersetCard n s ⊆ powersetCard n t :=
  fun _u h' => mem_powersetCard.2 <|
    And.imp (fun h₂ => Subset.trans h₂ h) id (mem_powersetCard.1 h')

Monotonicity of Fixed-Size Subsets: $\text{powersetCard}_n(s) \subseteq \text{powersetCard}_n(t)$ when $s \subseteq t$

Informal description

For any natural number $n$ and finite sets $s, t$ of type $\alpha$, if $s \subseteq t$, then the set of all subsets of $s$ with exactly $n$ elements is a subset of the set of all subsets of $t$ with exactly $n$ elements. In other words: $$ s \subseteq t \implies \text{powersetCard}_n(s) \subseteq \text{powersetCard}_n(t) $$

Finset.card_powersetCard theorem

(n : ℕ) (s : Finset α) : card (powersetCard n s) = Nat.choose (card s) n

Full source

/-- **Formula for the Number of Combinations** -/
@[simp]
theorem card_powersetCard (n : ℕ) (s : Finset α) :
    card (powersetCard n s) = Nat.choose (card s) n :=
  (card_pmap _ _ _).trans (Multiset.card_powersetCard n s.1)

Cardinality of Fixed-Size Subsets Formula: $\text{card}(\text{powersetCard}_n(s)) = \binom{|s|}{n}$

Informal description

For any natural number $n$ and finite set $s$ of type $\alpha$, the number of subsets of $s$ with exactly $n$ elements is equal to the binomial coefficient $\binom{|s|}{n}$, where $|s|$ denotes the cardinality of $s$.

Finset.powersetCard_zero theorem

(s : Finset α) : s.powersetCard 0 = {∅}

Full source

@[simp]
theorem powersetCard_zero (s : Finset α) : s.powersetCard 0 = {∅} := by
  ext; rw [mem_powersetCard, mem_singleton, card_eq_zero]
  refine
    ⟨fun h => h.2, fun h => by
      rw [h]
      exact ⟨empty_subset s, rfl⟩⟩

$\text{powersetCard}_0(s) = \{\emptyset\}$ for any finite set $s$

Informal description

For any finite set $s$ of type $\alpha$, the set of all subsets of $s$ with cardinality $0$ is equal to the singleton set containing the empty set, i.e., $\text{powersetCard}_0(s) = \{\emptyset\}$.

Finset.powersetCard_empty_subsingleton theorem

(n : ℕ) : (powersetCard n (∅ : Finset α) : Set <| Finset α).Subsingleton

Full source

lemma powersetCard_empty_subsingleton (n : ℕ) :
    (powersetCard n (∅ : Finset α) : Set <| Finset α).Subsingleton := by
  simp [Set.Subsingleton, subset_empty]

Subsingleton Property of Fixed-Cardinality Subsets of the Empty Set

Informal description

For any natural number $n$, the set of all subsets with cardinality $n$ of the empty finite set is a subsingleton (i.e., contains at most one element).

Finset.map_val_val_powersetCard theorem

(s : Finset α) (i : ℕ) : (s.powersetCard i).val.map Finset.val = s.1.powersetCard i

Full source

@[simp]
theorem map_val_val_powersetCard (s : Finset α) (i : ℕ) :
    (s.powersetCard i).val.map Finset.val = s.1.powersetCard i := by
  simp [Finset.powersetCard, map_pmap, pmap_eq_map, map_id']

Equality of Multiset Mappings for Fixed-Cardinality Subsets

Informal description

For any finite set $s$ of type $\alpha$ and any natural number $i$, the multiset obtained by applying the underlying multiset map to the elements of $s.\text{powersetCard}(i)$ is equal to $s.1.\text{powersetCard}(i)$. In other words, if we take all subsets of $s$ with cardinality $i$ (as a finset), extract their underlying multisets, and collect these into a multiset, the result is the same as directly computing the multiset of all submultisets of $s$'s underlying multiset with cardinality $i$.

Finset.powersetCard_one theorem

(s : Finset α) : s.powersetCard 1 = s.map ⟨_, Finset.singleton_injective⟩

Full source

theorem powersetCard_one (s : Finset α) :
    s.powersetCard 1 = s.map ⟨_, Finset.singleton_injective⟩ :=
  eq_of_veq <| Multiset.map_injective val_injective <| by simp [Multiset.powersetCard_one]

One-element subsets are singletons

Informal description

For any finite set $s$ of type $\alpha$, the set of all subsets of $s$ with exactly one element is equal to the image of $s$ under the singleton map. That is, $\text{powersetCard}(1, s) = \{ \{a\} \mid a \in s \}$.

Finset.powersetCard_eq_empty theorem

: powersetCard n s = ∅ ↔ s.card < n

Full source

@[simp]
lemma powersetCard_eq_empty : powersetCardpowersetCard n s = ∅ ↔ s.card < n := by
  refine ⟨?_, fun h ↦ card_eq_zero.1 <| by rw [card_powersetCard, Nat.choose_eq_zero_of_lt h]⟩
  contrapose!
  exact fun h ↦ nonempty_iff_ne_empty.1 <| (exists_subset_card_eq h).imp <| by simp

Emptyness of Fixed-Size Subsets: $\text{powersetCard}_n(s) = \emptyset \iff |s| < n$

Informal description

For any natural number $n$ and finite set $s$, the set of all subsets of $s$ with exactly $n$ elements is empty if and only if the cardinality of $s$ is less than $n$. In other words: $$\text{powersetCard}_n(s) = \emptyset \iff |s| < n$$

Finset.powersetCard_card_add theorem

(s : Finset α) (hn : 0 < n) : s.powersetCard (s.card + n) = ∅

Full source

@[simp] lemma powersetCard_card_add (s : Finset α) (hn : 0 < n) :
    s.powersetCard (s.card + n) = ∅ := by simpa

Emptyness of Subsets with Cardinality Exceeding the Base Set

Informal description

For any finite set $s$ of type $\alpha$ and any positive natural number $n$, the set of all subsets of $s$ with exactly $s.\text{card} + n$ elements is empty. That is, $\text{powersetCard}(s.\text{card} + n, s) = \emptyset$.

Finset.powersetCard_eq_filter theorem

{n} {s : Finset α} : powersetCard n s = (powerset s).filter fun x => x.card = n

Full source

theorem powersetCard_eq_filter {n} {s : Finset α} :
    powersetCard n s = (powerset s).filter fun x => x.card = n := by
  ext
  simp [mem_powersetCard]

Characterization of Fixed-Size Subsets via Power Set Filtering

Informal description

For any natural number $n$ and finite set $s$ of type $\alpha$, the set of all subsets of $s$ with exactly $n$ elements is equal to the set obtained by filtering the power set of $s$ to retain only those subsets whose cardinality is $n$. In other words: $$\text{powersetCard } n \ s = \{x \in \text{powerset } s \mid |x| = n\}$$

Finset.powersetCard_succ_insert theorem

 [DecidableEq α] {x : α} {s : Finset α} (h : x ∉ s) (n : ℕ) :
  powersetCard n.succ (insert x s) = powersetCard n.succ s ∪ (powersetCard n s).image (insert x)

Full source

theorem powersetCard_succ_insert [DecidableEq α] {x : α} {s : Finset α} (h : x ∉ s) (n : ℕ) :
    powersetCard n.succ (insert x s) =
    powersetCardpowersetCard n.succ s ∪ (powersetCard n s).image (insert x) := by
  rw [powersetCard_eq_filter, powerset_insert, filter_union, ← powersetCard_eq_filter]
  congr
  rw [powersetCard_eq_filter, filter_image]
  congr 1
  ext t
  simp only [mem_powerset, mem_filter, Function.comp_apply, and_congr_right_iff]
  intro ht
  have : x ∉ t := fun H => h (ht H)
  simp [card_insert_of_not_mem this, Nat.succ_inj]

Recursive Construction of $(n+1)$-Element Subsets via Insertion

Informal description

For any finite set $s$ of type $\alpha$ with decidable equality, any element $x \notin s$, and any natural number $n$, the set of all subsets of $s \cup \{x\}$ with exactly $n+1$ elements is equal to the union of: 1. The set of all subsets of $s$ with exactly $n+1$ elements, and 2. The image under the insertion of $x$ of the set of all subsets of $s$ with exactly $n$ elements. In other words: $$\mathcal{P}_{n+1}(s \cup \{x\}) = \mathcal{P}_{n+1}(s) \cup \{ t \cup \{x\} \mid t \in \mathcal{P}_n(s) \}$$

Finset.powersetCard_nonempty theorem

: (powersetCard n s).Nonempty ↔ n ≤ s.card

Full source

@[simp]
lemma powersetCard_nonempty : (powersetCard n s).Nonempty ↔ n ≤ s.card := by
  aesop (add simp [Finset.Nonempty, exists_subset_card_eq, card_le_card])

Nonemptiness of Fixed-Cardinality Subsets of a Finite Set

Informal description

For a finite set $s$ and a natural number $n$, the set of all subsets of $s$ with exactly $n$ elements is nonempty if and only if $n$ is less than or equal to the cardinality of $s$.

Finset.powersetCard_self theorem

(s : Finset α) : powersetCard s.card s = { s }

Full source

@[simp]
theorem powersetCard_self (s : Finset α) : powersetCard s.card s = {s} := by
  ext
  rw [mem_powersetCard, mem_singleton]
  constructor
  · exact fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge
  · rintro rfl
    simp

Fixed-Cardinality Powerset of a Finite Set is Singleton

Informal description

For any finite set $s$ of type $\alpha$, the set of all subsets of $s$ with cardinality equal to the cardinality of $s$ is exactly the singleton set $\{s\}$. In other words: $$\mathcal{P}_{|s|}(s) = \{s\}$$

Finset.pairwise_disjoint_powersetCard theorem

(s : Finset α) : Pairwise fun i j => Disjoint (s.powersetCard i) (s.powersetCard j)

Full source

theorem pairwise_disjoint_powersetCard (s : Finset α) :
    Pairwise fun i j => Disjoint (s.powersetCard i) (s.powersetCard j) := fun _i _j hij =>
  Finset.disjoint_left.mpr fun _x hi hj =>
    hij <| (mem_powersetCard.mp hi).2.symm.trans (mem_powersetCard.mp hj).2

Pairwise Disjointness of Fixed-Cardinality Subsets of a Finite Set

Informal description

For any finite set $s$ of type $\alpha$, the family of sets $\{\text{powersetCard}_i(s) \mid i \in \mathbb{N}\}$ is pairwise disjoint. That is, for any two distinct natural numbers $i$ and $j$, the sets $\text{powersetCard}_i(s)$ and $\text{powersetCard}_j(s)$ are disjoint.

Finset.powerset_card_disjiUnion theorem

 (s : Finset α) :
  Finset.powerset s =
    (range (s.card + 1)).disjiUnion (fun i => powersetCard i s) (s.pairwise_disjoint_powersetCard.set_pairwise _)

Full source

theorem powerset_card_disjiUnion (s : Finset α) :
    Finset.powerset s =
      (range (s.card + 1)).disjiUnion (fun i => powersetCard i s)
        (s.pairwise_disjoint_powersetCard.set_pairwise _) := by
  refine ext fun a => ⟨fun ha => ?_, fun ha => ?_⟩
  · rw [mem_disjiUnion]
    exact
      ⟨a.card, mem_range.mpr (Nat.lt_succ_of_le (card_le_card (mem_powerset.mp ha))),
        mem_powersetCard.mpr ⟨mem_powerset.mp ha, rfl⟩⟩
  · rcases mem_disjiUnion.mp ha with ⟨i, _hi, ha⟩
    exact mem_powerset.mpr (mem_powersetCard.mp ha).1

Decomposition of Power Set into Disjoint Union of Fixed-Cardinality Subsets

Informal description

For any finite set $s$ of type $\alpha$, the power set of $s$ is equal to the disjoint union of all subsets of $s$ with cardinality $i$, where $i$ ranges from $0$ to the cardinality of $s$ (inclusive). That is, $$\mathcal{P}(s) = \bigsqcup_{i=0}^{|s|} \mathcal{P}_i(s),$$ where $\mathcal{P}_i(s)$ denotes the set of all subsets of $s$ with exactly $i$ elements, and the union is disjoint since $\mathcal{P}_i(s)$ and $\mathcal{P}_j(s)$ are disjoint for $i \neq j$.

Finset.powerset_card_biUnion theorem

[DecidableEq (Finset α)] (s : Finset α) : Finset.powerset s = (range (s.card + 1)).biUnion fun i => powersetCard i s

Full source

theorem powerset_card_biUnion [DecidableEq (Finset α)] (s : Finset α) :
    Finset.powerset s = (range (s.card + 1)).biUnion fun i => powersetCard i s := by
  simpa only [disjiUnion_eq_biUnion] using powerset_card_disjiUnion s

Power Set as Union of Fixed-Cardinality Subsets

Informal description

For any finite set $s$ of type $\alpha$ with decidable equality, the power set of $s$ is equal to the union over all $i$ from $0$ to $|s|$ (inclusive) of the sets of subsets of $s$ with exactly $i$ elements. That is, $$\mathcal{P}(s) = \bigcup_{i=0}^{|s|} \{ t \subseteq s \mid |t| = i \}.$$

Finset.powersetCard_sup theorem

[DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.card) : (powersetCard n.succ u).sup id = u

Full source

theorem powersetCard_sup [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.card) :
    (powersetCard n.succ u).sup id = u := by
  apply le_antisymm
  · simp_rw [Finset.sup_le_iff, mem_powersetCard]
    rintro x ⟨h, -⟩
    exact h
  · rw [sup_eq_biUnion, le_iff_subset, subset_iff]
    intro x hx
    simp only [mem_biUnion, exists_prop, id]
    obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetCard n (u.erase x) := powersetCard_nonempty.2
      (le_trans (Nat.le_sub_one_of_lt hn) pred_card_le_card_erase)
    refine ⟨insert x t, ?_, mem_insert_self _ _⟩
    rw [← insert_erase hx, powersetCard_succ_insert (not_mem_erase _ _)]
    exact mem_union_right _ (mem_image_of_mem _ ht)

Supremum of $(n+1)$-element subsets equals original set

Informal description

For any finite set $u$ of type $\alpha$ with decidable equality and any natural number $n$ such that $n < |u|$, the supremum (under the subset order) of all subsets of $u$ with exactly $n+1$ elements is equal to $u$ itself. In other words: $$ \sup \{ t \subseteq u \mid |t| = n+1 \} = u $$

Finset.powersetCard_map theorem

 {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α) :
  powersetCard n (s.map f) = (powersetCard n s).map (mapEmbedding f).toEmbedding

Full source

theorem powersetCard_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α) :
    powersetCard n (s.map f) = (powersetCard n s).map (mapEmbedding f).toEmbedding :=
  ext fun t => by
    -- `le_eq_subset` is a dangerous lemma since it turns the type `↪o` into `(· ⊆ ·) ↪r (· ⊆ ·)`,
    -- which makes `simp` have trouble working with `mapEmbedding_apply`.
    simp only [mem_powersetCard, mem_map, RelEmbedding.coe_toEmbedding, mapEmbedding_apply]
    constructor
    · classical
      intro h
      have : map f (filter (fun x => (f x ∈ t)) s) = t := by
        ext x
        simp only [mem_map, mem_filter, decide_eq_true_eq]
        exact ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂,
          fun hx => let ⟨y, hy⟩ := mem_map.1 (h.1 hx); ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
      refine ⟨_, ?_, this⟩
      rw [← card_map f, this, h.2]; simp
    · rintro ⟨a, ⟨has, rfl⟩, rfl⟩
      simp only [map_subset_map, has, card_map, and_self]

Mapping Preserves Fixed-Cardinality Subsets under Injective Embedding

Informal description

Let $\alpha$ and $\beta$ be types, and let $f : \alpha \hookrightarrow \beta$ be an injective function embedding. For any natural number $n$ and any finite set $s \subseteq \alpha$, the set of all subsets of $s$ with exactly $n$ elements, when mapped under $f$, is equal to the set of all subsets of $f(s)$ with exactly $n$ elements. In other words, the following equality holds for the finite set operations: $$ \text{powersetCard}_n (s \text{.map } f) = (\text{powersetCard}_n s) \text{.map } f $$