changeset 40311 | 994e784ca17a |
parent 39302 | d7728f65b353 |
child 40702 | cf26dd7395e4 |
--- a/src/HOL/Finite_Set.thy Tue Nov 02 21:59:21 2010 +0100 +++ b/src/HOL/Finite_Set.thy Wed Nov 03 08:29:32 2010 +0100 @@ -2182,7 +2182,7 @@ subsubsection {* Pigeonhole Principles *} -lemma pigeonhole: "finite(A) \<Longrightarrow> card A > card(f ` A) \<Longrightarrow> ~ inj_on f A " +lemma pigeonhole: "card A > card(f ` A) \<Longrightarrow> ~ inj_on f A " by (auto dest: card_image less_irrefl_nat) lemma pigeonhole_infinite: