equal
deleted
inserted
replaced
998 |
998 |
999 lemma bex_imageD: |
999 lemma bex_imageD: |
1000 assumes "\<exists>x\<in>f ` A. P x" |
1000 assumes "\<exists>x\<in>f ` A. P x" |
1001 shows "\<exists>x\<in>A. P (f x)" |
1001 shows "\<exists>x\<in>A. P (f x)" |
1002 using assms by auto |
1002 using assms by auto |
|
1003 |
|
1004 lemma image_add_0 [simp]: "op+ (0::'a::comm_monoid_add) ` S = S" |
|
1005 by auto |
1003 |
1006 |
1004 |
1007 |
1005 text \<open> |
1008 text \<open> |
1006 \medskip Range of a function -- just a translation for image! |
1009 \medskip Range of a function -- just a translation for image! |
1007 \<close> |
1010 \<close> |