Mathlib.Data.Fintype.Powerset

Finset.fintype instance

[Fintype α] : Fintype (Finset α)

Full source

instance Finset.fintype [Fintype α] : Fintype (Finset α) :=
  ⟨univ.powerset, fun _ => Finset.mem_powerset.2 (Finset.subset_univ _)⟩

Finite Subsets of a Finite Type Form a Finite Type

Informal description

For any finite type $\alpha$, the type of finite subsets of $\alpha$ is also finite.

Fintype.card_finset theorem

[Fintype α] : Fintype.card (Finset α) = 2 ^ Fintype.card α

Full source

@[simp]
theorem Fintype.card_finset [Fintype α] : Fintype.card (Finset α) = 2 ^ Fintype.card α :=
  Finset.card_powerset Finset.univ

Cardinality of Finite Subsets: $|\mathcal{F}(\alpha)| = 2^{|\alpha|}$

Informal description

For any finite type $\alpha$, the cardinality of the type of finite subsets of $\alpha$ is $2^n$, where $n$ is the cardinality of $\alpha$.

Finset.powerset_univ theorem

: (univ : Finset α).powerset = univ

Full source

@[simp] lemma powerset_univ : (univ : Finset α).powerset = univ :=
  coe_injective <| by simp [-coe_eq_univ]

Powerset of Universal Finite Set Equals Universal Finite Set

Informal description

For a finite type $\alpha$, the powerset of the universal finite set `univ : Finset α` is equal to the universal finite set of type `Finset (Finset α)`. In other words, $\mathcal{P}(\text{univ}) = \text{univ}$ where $\mathcal{P}$ denotes the powerset operation and both `univ` refer to the universal finite sets of their respective types.

Finset.filter_subset_univ theorem

[DecidableEq α] (s : Finset α) : ({t | t ⊆ s} : Finset _) = powerset s

Full source

lemma filter_subset_univ [DecidableEq α] (s : Finset α) :
    ({t | t ⊆ s} : Finset _) = powerset s := by ext; simp

Subset Filter Equals Powerset for Finite Types

Informal description

For any finite type $\alpha$ with decidable equality and any finite subset $s$ of $\alpha$, the set of all finite subsets of $\alpha$ that are contained in $s$ is equal to the powerset of $s$.

Finset.powerset_eq_univ theorem

: s.powerset = univ ↔ s = univ

Full source

@[simp] lemma powerset_eq_univ : s.powerset = univ ↔ s = univ := by
  rw [← Finset.powerset_univ, powerset_inj]

Powerset Equals Universal Set if and only if Set is Universal

Informal description

For any finite subset $s$ of a finite type $\alpha$, the powerset of $s$ is equal to the universal finite set of type `Finset (Finset α)` if and only if $s$ is equal to the universal finite set of $\alpha$. In other words, $\mathcal{P}(s) = \text{univ} \leftrightarrow s = \text{univ}$, where $\mathcal{P}$ denotes the powerset operation and $\text{univ}$ refers to the universal finite set of the respective type.

Finset.mem_powersetCard_univ theorem

: s ∈ powersetCard k (univ : Finset α) ↔ #s = k

Full source

lemma mem_powersetCard_univ : s ∈ powersetCard k (univ : Finset α)s ∈ powersetCard k (univ : Finset α) ↔ #s = k :=
  mem_powersetCard.trans <| and_iff_right <| subset_univ _

Characterization of k-Element Subsets in a Finite Type

Informal description

For any finite subset $s$ of a finite type $\alpha$ and any natural number $k$, $s$ is an element of the set of all $k$-element subsets of the universal finite set of $\alpha$ if and only if the cardinality of $s$ is equal to $k$. In other words, $s \in \text{powersetCard}_k(\text{univ}) \leftrightarrow |s| = k$.

Finset.univ_filter_card_eq theorem

(k : ℕ) : ({s | #s = k} : Finset (Finset α)) = univ.powersetCard k

Full source

@[simp] lemma univ_filter_card_eq (k : ℕ) :
   ({s | #s = k} : Finset (Finset α)) = univ.powersetCard k := by ext; simp

Characterization of k-Element Subsets of a Finite Type

Informal description

For any natural number $k$ and any finite type $\alpha$, the set of all finite subsets of $\alpha$ with cardinality $k$ is equal to the set of all $k$-element subsets of the universal finite set of $\alpha$. In other words, $\{s \mid |s| = k\} = \text{powersetCard}_k(\text{univ})$.

Fintype.card_finset_len theorem

[Fintype α] (k : ℕ) : Fintype.card { s : Finset α // #s = k } = Nat.choose (Fintype.card α) k

Full source

@[simp]
theorem Fintype.card_finset_len [Fintype α] (k : ℕ) :
    Fintype.card { s : Finset α // #s = k } = Nat.choose (Fintype.card α) k := by
  simp [Fintype.subtype_card, Finset.card_univ]

Cardinality of k-Element Subsets of a Finite Type Equals Binomial Coefficient

Informal description

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

Set.fintype instance

[Fintype α] : Fintype (Set α)

Full source

instance Set.fintype [Fintype α] : Fintype (Set α) :=
  ⟨(@Finset.univ (Finset α) _).map coeEmb.1, fun s => by
    classical
    refine mem_map.2 ⟨({a | a ∈ s} : Finset _), Finset.mem_univ _, (coe_filter _ _).trans ?_⟩
    simp⟩

Finite Type of Sets over a Finite Type

Informal description

For any finite type $\alpha$, the type of sets over $\alpha$ is also finite.

Set.instFinite instance

[Finite α] : Finite (Set α)

Full source

instance Set.instFinite [Finite α] : Finite (Set α) := by
  cases nonempty_fintype α
  infer_instance

Finite Type of Sets over a Finite Type

Informal description

For any finite type $\alpha$, the type of sets over $\alpha$ is also finite.

Fintype.card_set theorem

[Fintype α] : Fintype.card (Set α) = 2 ^ Fintype.card α

Full source

@[simp]
theorem Fintype.card_set [Fintype α] : Fintype.card (Set α) = 2 ^ Fintype.card α :=
  (Finset.card_map _).trans (Finset.card_powerset _)

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

Informal description

For any finite type $\alpha$, the cardinality of the type of sets over $\alpha$ is $2^n$, where $n$ is the cardinality of $\alpha$.