feat(Set): Add Set.Finite.powerset (#14175)

If set `s` is finite, then powerset of `s` (`𝒫 s`) is finite.

Zulip: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Set.20is.20finite.2C.20then.20its.20powerset.20is.20finite/near/447338619

Recreate of #14173

Mathlib/Data/Set/Finite.lean

@@ -1035,6 +1035,9 @@ theorem Finite.finite_subsets {α : Type u} {a : Set α} (h : a.Finite) : { b |
     ← and_assoc, Finset.coeEmb] using h.subset
 #align set.finite.finite_subsets Set.Finite.finite_subsets
 
+protected theorem Finite.powerset {s : Set α} (h : s.Finite) : (𝒫 s).Finite :=
+  h.finite_subsets
+
 section Pi
 variable {ι : Type*} [Finite ι] {κ : ι → Type*} {t : ∀ i, Set (κ i)}