2163 unfolding bij_betw_def using finite_imageD [of f A] by auto |
2163 unfolding bij_betw_def using finite_imageD [of f A] by auto |
2164 |
2164 |
2165 lemma inj_on_finite: "inj_on f A \<Longrightarrow> f ` A \<le> B \<Longrightarrow> finite B \<Longrightarrow> finite A" |
2165 lemma inj_on_finite: "inj_on f A \<Longrightarrow> f ` A \<le> B \<Longrightarrow> finite B \<Longrightarrow> finite A" |
2166 using finite_imageD finite_subset by blast |
2166 using finite_imageD finite_subset by blast |
2167 |
2167 |
|
2168 lemma card_vimage_inj_on_le: |
|
2169 assumes "inj_on f D" "finite A" |
|
2170 shows "card (f-`A \<inter> D) \<le> card A" |
|
2171 proof (rule card_inj_on_le) |
|
2172 show "inj_on f (f -` A \<inter> D)" |
|
2173 by (blast intro: assms inj_on_subset) |
|
2174 qed (use assms in auto) |
|
2175 |
2168 lemma card_vimage_inj: "inj f \<Longrightarrow> A \<subseteq> range f \<Longrightarrow> card (f -` A) = card A" |
2176 lemma card_vimage_inj: "inj f \<Longrightarrow> A \<subseteq> range f \<Longrightarrow> card (f -` A) = card A" |
2169 by (auto 4 3 simp: subset_image_iff inj_vimage_image_eq |
2177 by (auto 4 3 simp: subset_image_iff inj_vimage_image_eq |
2170 intro: card_image[symmetric, OF subset_inj_on]) |
2178 intro: card_image[symmetric, OF subset_inj_on]) |
2171 |
|
2172 |
2179 |
2173 subsubsection \<open>Pigeonhole Principles\<close> |
2180 subsubsection \<open>Pigeonhole Principles\<close> |
2174 |
2181 |
2175 lemma pigeonhole: "card A > card (f ` A) \<Longrightarrow> \<not> inj_on f A " |
2182 lemma pigeonhole: "card A > card (f ` A) \<Longrightarrow> \<not> inj_on f A " |
2176 by (auto dest: card_image less_irrefl_nat) |
2183 by (auto dest: card_image less_irrefl_nat) |