src/HOL/Set.thy
changeset 31461 d54b743b52a3
parent 31456 55edadbd43d5
parent 31441 428e4caf2299
child 31643 b040f1679f77
     1.1 --- a/src/HOL/Set.thy	Fri Jun 05 08:00:53 2009 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Jun 05 08:06:03 2009 +0200
     1.3 @@ -1345,13 +1345,16 @@
     1.4  by auto
     1.5  
     1.6  lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
     1.7 -  by blast
     1.8 +by blast
     1.9  
    1.10  lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
    1.11 -  by blast
    1.12 +by blast
    1.13  
    1.14  lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
    1.15 -  by blast
    1.16 +by blast
    1.17 +
    1.18 +lemma empty_is_image[iff]: "({} = f ` A) = (A = {})"
    1.19 +by blast
    1.20  
    1.21  
    1.22  lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"