# 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.

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

There are finitely many subsets of a given finite set

source
theorem Set.Finite.powerset {α : Type u} {s : Set α} (h : s.Finite) :
(𝒫 s).Finite