在尝试证明某些事情时，我遇到了一个无辜的声称，即我未能在Coq中证明。有人声称，对于给定的有限合奏，幂集也是有限的。该声明在下面的Coq代码中给出。
我浏览了关于有限集的Coq文档以及关于有限集和幂集的事实，但是我找不到将幂集解构为子集的并集的东西（以便Union_is_finite可以使用构造函数）。另一种方法可能是显示幂集的基数为2 ^ | S |。但是在这里我当然不知道如何处理证明。
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.