# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1642439090 0
# Node ID ac3901e4e0a941383607d6a0a8d2f1c7f5fc977a
# Parent  192876ea202d693c268306efa5e50894f65568bc
A new lemma about inverse image

diff -r 192876ea202d -r ac3901e4e0a9 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sun Jan 16 21:41:16 2022 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Jan 17 17:04:50 2022 +0000
@@ -2165,11 +2165,18 @@
 lemma inj_on_finite: "inj_on f A \<Longrightarrow> f ` A \<le> B \<Longrightarrow> finite B \<Longrightarrow> finite A"
   using finite_imageD finite_subset by blast
 
+lemma card_vimage_inj_on_le:
+  assumes "inj_on f D" "finite A"
+  shows "card (f-`A \<inter> D) \<le> card A"
+proof (rule card_inj_on_le)
+  show "inj_on f (f -` A \<inter> D)"
+    by (blast intro: assms inj_on_subset)
+qed (use assms in auto)
+
 lemma card_vimage_inj: "inj f \<Longrightarrow> A \<subseteq> range f \<Longrightarrow> card (f -` A) = card A"
   by (auto 4 3 simp: subset_image_iff inj_vimage_image_eq
       intro: card_image[symmetric, OF subset_inj_on])
 
-
 subsubsection \<open>Pigeonhole Principles\<close>
 
 lemma pigeonhole: "card A > card (f ` A) \<Longrightarrow> \<not> inj_on f A "