# HG changeset patch
# User nipkow
# Date 1743605796 -7200
# Node ID 00a83dd881416f068e3d725b333b8eb916095fd1
# Parent  88064da0ae76ac6f98fd3e77585c0b7189a6e166
Added lemma

diff -r 88064da0ae76 -r 00a83dd88141 src/HOL/Library/Infinite_Typeclass.thy
--- 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)