# HG changeset patch
# User Andreas Lochbihler
# Date 1423566264 -3600
# Node ID 8a183caa424dc488c5ddd99699db01de79ed3242
# Parent  adaa430fc0f7665a7bb532ad46a178c2fa6c7ad5
add stronger version of lemma

diff -r adaa430fc0f7 -r 8a183caa424d src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Fri Feb 06 17:57:03 2015 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Tue Feb 10 12:04:24 2015 +0100
@@ -143,23 +143,33 @@
   contains some element that occurs infinitely often.
 *}
 
+lemma inf_img_fin_dom':
+  assumes img: "finite (f ` A)" and dom: "infinite A"
+  shows "\<exists>y \<in> f ` A. infinite (f -` {y} \<inter> A)"
+proof (rule ccontr)
+  have "A \<subseteq> (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by auto
+  moreover
+  assume "\<not> ?thesis"
+  with img have "finite (\<Union>y\<in>f ` A. f -` {y} \<inter> A)" by blast
+  ultimately have "finite A" by(rule finite_subset)
+  with dom show False by contradiction
+qed
+
+lemma inf_img_fin_domE':
+  assumes "finite (f ` A)" and "infinite A"
+  obtains y where "y \<in> f`A" and "infinite (f -` {y} \<inter> A)"
+  using assms by (blast dest: inf_img_fin_dom')
+
 lemma inf_img_fin_dom:
   assumes img: "finite (f`A)" and dom: "infinite A"
   shows "\<exists>y \<in> f`A. infinite (f -` {y})"
-proof (rule ccontr)
-  assume "\<not> ?thesis"
-  with img have "finite (UN y:f`A. f -` {y})" by blast
-  moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto
-  moreover note dom
-  ultimately show False by (simp add: infinite_super)
-qed
+using inf_img_fin_dom'[OF assms] by auto
 
 lemma inf_img_fin_domE:
   assumes "finite (f`A)" and "infinite A"
   obtains y where "y \<in> f`A" and "infinite (f -` {y})"
   using assms by (blast dest: inf_img_fin_dom)
 
-
 subsection "Infinitely Many and Almost All"
 
 text {*