src/HOL/Set.thy
changeset 26150 f6bd8686b71e
parent 25965 05df64f786a4
child 26339 7825c83c9eff
     1.1 --- a/src/HOL/Set.thy	Tue Feb 26 20:38:14 2008 +0100
     1.2 +++ b/src/HOL/Set.thy	Tue Feb 26 20:38:15 2008 +0100
     1.3 @@ -645,6 +645,9 @@
     1.4  lemma bex_UNIV [simp]: "Bex UNIV P = Ex P"
     1.5    by (simp add: Bex_def)
     1.6  
     1.7 +lemma UNIV_eq_I: "(\<And>x. x \<in> A) \<Longrightarrow> UNIV = A"
     1.8 +  by auto
     1.9 +
    1.10  
    1.11  subsubsection {* The empty set *}
    1.12  
    1.13 @@ -953,6 +956,9 @@
    1.14  lemma image_Un: "f`(A Un B) = f`A Un f`B"
    1.15    by blast
    1.16  
    1.17 +lemma image_eq_UN: "f`A = (UN x:A. {f x})"
    1.18 +  by blast
    1.19 +
    1.20  lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
    1.21    by blast
    1.22  
    1.23 @@ -2110,6 +2116,24 @@
    1.24    -- {* monotonicity *}
    1.25    by blast
    1.26  
    1.27 +lemma vimage_image_eq [noatp]: "f -` (f ` A) = {y. EX x:A. f x = f y}"
    1.28 +by (blast intro: sym)
    1.29 +
    1.30 +lemma image_vimage_subset: "f ` (f -` A) <= A"
    1.31 +by blast
    1.32 +
    1.33 +lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
    1.34 +by blast
    1.35 +
    1.36 +lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
    1.37 +by blast
    1.38 +
    1.39 +lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
    1.40 +by blast
    1.41 +
    1.42 +lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
    1.43 +by blast
    1.44 +
    1.45  
    1.46  subsection {* Getting the Contents of a Singleton Set *}
    1.47