diff -r 6d158fd15b85 -r 8230dca028eb src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Jan 24 10:04:32 2019 +0100
+++ b/src/HOL/Fun.thy	Thu Jan 24 14:44:52 2019 +0000
@@ -292,6 +292,13 @@
    by (rule linorder_cases) (auto dest: assms simp: that)
 qed
 
+
+lemma inj_on_image_Pow: "inj_on f A \<Longrightarrow>inj_on (image f) (Pow A)"
+  unfolding Pow_def inj_on_def by blast
+
+lemma bij_betw_image_Pow: "bij_betw f A B \<Longrightarrow> bij_betw (image f) (Pow A) (Pow B)"
+  by (auto simp add: bij_betw_def inj_on_image_Pow image_Pow_surj)
+
 lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
   by auto