equal
deleted
inserted
replaced
337 lemma inf_img_fin_dom: |
337 lemma inf_img_fin_dom: |
338 assumes img: "finite (f`A)" and dom: "infinite A" |
338 assumes img: "finite (f`A)" and dom: "infinite A" |
339 shows "\<exists>y \<in> f`A. infinite (f -` {y})" |
339 shows "\<exists>y \<in> f`A. infinite (f -` {y})" |
340 proof (rule ccontr) |
340 proof (rule ccontr) |
341 assume "\<not> ?thesis" |
341 assume "\<not> ?thesis" |
342 with img have "finite (UN y:f`A. f -` {y})" by (blast intro: finite_UN_I) |
342 with img have "finite (UN y:f`A. f -` {y})" by blast |
343 moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto |
343 moreover have "A \<subseteq> (UN y:f`A. f -` {y})" by auto |
344 moreover note dom |
344 moreover note dom |
345 ultimately show False by (simp add: infinite_super) |
345 ultimately show False by (simp add: infinite_super) |
346 qed |
346 qed |
347 |
347 |