--- a/src/HOL/Library/Infinite_Typeclass.thy Tue Apr 01 12:10:45 2025 +0200
+++ b/src/HOL/Library/Infinite_Typeclass.thy Wed Apr 02 16:56:36 2025 +0200
@@ -27,6 +27,9 @@
by auto
qed
+lemma arb_inj_on_finite_infinite: "finite(A :: 'b set) \<Longrightarrow> \<exists>f :: 'b \<Rightarrow> 'a. inj_on f A"
+by (meson arb_finite_subset card_le_inj infinite_imp_nonempty)
+
lemma arb_countable_map: "finite Y \<Longrightarrow> \<exists>f :: (nat \<Rightarrow> 'a). inj f \<and> range f \<subseteq> UNIV - Y"
using infinite_UNIV
by (auto simp: infinite_countable_subset)