From 270043b5b75c5d667ebcf747e4ab3a108e453205 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?SnO=E2=82=82WMaN?= <me@sno2wman.net>
Date: Wed, 26 Jun 2024 23:14:03 +0000
Subject: [PATCH] feat(Set): Add `Set.Finite.powerset` (#14175)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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 | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean
index a4ebbed313a99..f2f150c744389 100644
--- a/Mathlib/Data/Set/Finite.lean
+++ b/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)}