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}. *}