diff -r 6d158fd15b85 -r 8230dca028eb src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Jan 24 10:04:32 2019 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Jan 24 14:44:52 2019 +0000
@@ -2182,4 +2182,35 @@
   for S :: "'a::linordered_ring set"
   by (rule ccontr) (auto simp: abs_eq_iff vimage_def dest: inf_img_fin_dom)
 
+subsection \<open>The finite powerset operator\<close>
+
+definition Fpow :: "'a set \<Rightarrow> 'a set set"
+where "Fpow A \<equiv> {X. X \<subseteq> A \<and> finite X}"
+
+lemma Fpow_mono: "A \<subseteq> B \<Longrightarrow> Fpow A \<subseteq> Fpow B"
+unfolding Fpow_def by auto
+
+lemma empty_in_Fpow: "{} \<in> Fpow A"
+unfolding Fpow_def by auto
+
+lemma Fpow_not_empty: "Fpow A \<noteq> {}"
+using empty_in_Fpow by blast
+
+lemma Fpow_subset_Pow: "Fpow A \<subseteq> Pow A"
+unfolding Fpow_def by auto
+
+lemma Fpow_Pow_finite: "Fpow A = Pow A Int {A. finite A}"
+unfolding Fpow_def Pow_def by blast
+
+lemma inj_on_image_Fpow:
+  assumes "inj_on f A"
+  shows "inj_on (image f) (Fpow A)"
+  using assms Fpow_subset_Pow[of A] subset_inj_on[of "image f" "Pow A"]
+    inj_on_image_Pow by blast
+
+lemma image_Fpow_mono:
+  assumes "f ` A \<subseteq> B"
+  shows "(image f) ` (Fpow A) \<subseteq> Fpow B"
+  using assms by(unfold Fpow_def, auto)
+
 end