equal
deleted
inserted
replaced
2180 by (auto intro: le_antisym card_inj_on_le) |
2180 by (auto intro: le_antisym card_inj_on_le) |
2181 |
2181 |
2182 |
2182 |
2183 subsubsection {* Pigeonhole Principles *} |
2183 subsubsection {* Pigeonhole Principles *} |
2184 |
2184 |
2185 lemma pigeonhole: "finite(A) \<Longrightarrow> card A > card(f ` A) \<Longrightarrow> ~ inj_on f A " |
2185 lemma pigeonhole: "card A > card(f ` A) \<Longrightarrow> ~ inj_on f A " |
2186 by (auto dest: card_image less_irrefl_nat) |
2186 by (auto dest: card_image less_irrefl_nat) |
2187 |
2187 |
2188 lemma pigeonhole_infinite: |
2188 lemma pigeonhole_infinite: |
2189 assumes "~ finite A" and "finite(f`A)" |
2189 assumes "~ finite A" and "finite(f`A)" |
2190 shows "EX a0:A. ~finite{a:A. f a = f a0}" |
2190 shows "EX a0:A. ~finite{a:A. f a = f a0}" |