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.

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

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