While trying to prove some things, I encountered an innocent looking claim that I failed to prove in Coq. The claim is that for a given Finite Ensemble, the powerset is also finite. The statement is given in the Coq code below.
I looked through the Coq documentation on finite sets and facts about finite sets and powersets, but I could not find something that deconstructs the powerset into a union of subsets (such that the Union_is_finite
constructor can be used). Another approach may be to show that the cardinal number of the powerset is 2^|S| but here I certainly have no idea how to approach the proof.
From Coq Require Export Sets.Ensembles.
From Coq Require Export Sets.Powerset.
From Coq Require Export Sets.Finite_sets.
Lemma powerset_finite {T} (S : Ensemble T) :
Finite T S -> Finite (Ensemble T) (Power_set T S).
Proof.
(* I don't know how to proceed. *)
Admitted.
powerset
of a finite set is also a finite set. But it relies on a different representation of finite sets, namely as ordered lists. Your result will certainly need the extensionality axiom for ensembles (Extensionality_Ensembles
), and maybe also classical logic. – Hemangioma