Mathlib.Data.Set.Finite.Powerset

Module docstring

{"# Finiteness of the powerset of a finite set

Implementation notes

Each result in this file should come in three forms: a Fintype instance, a Finite instance and a Set.Finite constructor.

Tags

finite sets ","### Constructors for Set.Finite

Every constructor here should have a corresponding Fintype instance in the Fintype module.

The implementation of these constructors ideally should be no more than Set.toFinite, after possibly setting up some Fintype and classical Decidable instances. "}

Set.Finite.finite_subsets theorem

{α : Type u} {a : Set α} (h : a.Finite) : {b | b ⊆ a}.Finite

Full source

/-- There are finitely many subsets of a given finite set -/
theorem Finite.finite_subsets {α : Type u} {a : Set α} (h : a.Finite) : { b | b ⊆ a }.Finite := by
  convert ((Finset.powerset h.toFinset).map Finset.coeEmb.1).finite_toSet
  ext s
  simpa [← @exists_finite_iff_finset α fun t => t ⊆ at ⊆ a ∧ t = s, Finite.subset_toFinset,
    ← and_assoc, Finset.coeEmb] using h.subset

Finiteness of the Power Set of a Finite Set

Informal description

For any finite set $a$ in a type $\alpha$, the collection of all subsets of $a$ is finite.

Set.Finite.powerset theorem

{s : Set α} (h : s.Finite) : (𝒫 s).Finite

Full source

protected theorem Finite.powerset {s : Set α} (h : s.Finite) : (𝒫 s).Finite :=
  h.finite_subsets

Finiteness of the Power Set of a Finite Set

Informal description

For any finite set $s$ in a type $\alpha$, the power set $\mathcal{P}(s)$ is finite.