src/HOL/Set.thy
 changeset 40703 d1fc454d6735 parent 39910 10097e0a9dbd child 40872 7c556a9240de
```     1.1 --- a/src/HOL/Set.thy	Mon Nov 22 10:34:33 2010 +0100
1.2 +++ b/src/HOL/Set.thy	Tue Nov 23 14:14:17 2010 +0100
1.3 @@ -622,6 +622,8 @@
1.4  lemma Pow_top: "A \<in> Pow A"
1.5    by simp
1.6
1.7 +lemma Pow_not_empty: "Pow A \<noteq> {}"
1.8 +  using Pow_top by blast
1.9
1.10  subsubsection {* Set complement *}
1.11
1.12 @@ -972,6 +974,21 @@
1.13  lemmas [symmetric, rulify] = atomize_ball
1.14    and [symmetric, defn] = atomize_ball
1.15
1.16 +lemma image_Pow_mono:
1.17 +  assumes "f ` A \<le> B"
1.18 +  shows "(image f) ` (Pow A) \<le> Pow B"
1.19 +using assms by blast
1.20 +
1.21 +lemma image_Pow_surj:
1.22 +  assumes "f ` A = B"
1.23 +  shows "(image f) ` (Pow A) = Pow B"
1.24 +using assms unfolding Pow_def proof(auto)
1.25 +  fix Y assume *: "Y \<le> f ` A"
1.26 +  obtain X where X_def: "X = {x \<in> A. f x \<in> Y}" by blast
1.27 +  have "f ` X = Y \<and> X \<le> A" unfolding X_def using * by auto
1.28 +  thus "Y \<in> (image f) ` {X. X \<le> A}" by blast
1.29 +qed
1.30 +
1.31  subsubsection {* Derived rules involving subsets. *}
1.32
1.33  text {* @{text insert}. *}
```