--- a/src/HOL/Finite_Set.thy Sun Oct 03 21:29:34 2021 +0200
+++ b/src/HOL/Finite_Set.thy Mon Oct 04 12:32:50 2021 +0100
@@ -373,6 +373,17 @@
lemma finite_vimage_iff: "bij h \<Longrightarrow> finite (h -` F) \<longleftrightarrow> finite F"
unfolding bij_def by (auto elim: finite_vimageD finite_vimageI)
+lemma finite_inverse_image_gen:
+ assumes "finite A" "inj_on f D"
+ shows "finite {j\<in>D. f j \<in> A}"
+ using finite_vimage_IntI [OF assms]
+ by (simp add: Collect_conj_eq inf_commute vimage_def)
+
+lemma finite_inverse_image:
+ assumes "finite A" "inj f"
+ shows "finite {j. f j \<in> A}"
+ using finite_inverse_image_gen [OF assms] by simp
+
lemma finite_Collect_bex [simp]:
assumes "finite A"
shows "finite {x. \<exists>y\<in>A. Q x y} \<longleftrightarrow> (\<forall>y\<in>A. finite {x. Q x y})"