--- a/src/HOL/Hilbert_Choice.thy Wed Apr 17 17:48:28 2019 +0100
+++ b/src/HOL/Hilbert_Choice.thy Wed Apr 17 21:53:45 2019 +0100
@@ -562,6 +562,27 @@
shows "inv f = g"
using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
+lemma subset_image_inj:
+ "S \<subseteq> f ` T \<longleftrightarrow> (\<exists>U. U \<subseteq> T \<and> inj_on f U \<and> S = f ` U)"
+proof safe
+ show "\<exists>U\<subseteq>T. inj_on f U \<and> S = f ` U"
+ if "S \<subseteq> f ` T"
+ proof -
+ from that [unfolded subset_image_iff subset_iff]
+ obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> x = f (g x)"
+ by (auto simp add: image_iff Bex_def choice_iff')
+ show ?thesis
+ proof (intro exI conjI)
+ show "g ` S \<subseteq> T"
+ by (simp add: g image_subsetI)
+ show "inj_on f (g ` S)"
+ using g by (auto simp: inj_on_def)
+ show "S = f ` (g ` S)"
+ using g image_subset_iff by auto
+ qed
+ qed
+qed blast
+
subsection \<open>Other Consequences of Hilbert's Epsilon\<close>
--- a/src/HOL/Library/Infinite_Set.thy Wed Apr 17 17:48:28 2019 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Wed Apr 17 21:53:45 2019 +0100
@@ -8,27 +8,6 @@
imports Main
begin
-lemma subset_image_inj:
- "S \<subseteq> f ` T \<longleftrightarrow> (\<exists>U. U \<subseteq> T \<and> inj_on f U \<and> S = f ` U)"
-proof safe
- show "\<exists>U\<subseteq>T. inj_on f U \<and> S = f ` U"
- if "S \<subseteq> f ` T"
- proof -
- from that [unfolded subset_image_iff subset_iff]
- obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> g x \<in> T \<and> x = f (g x)"
- unfolding image_iff by metis
- show ?thesis
- proof (intro exI conjI)
- show "g ` S \<subseteq> T"
- by (simp add: g image_subsetI)
- show "inj_on f (g ` S)"
- using g by (auto simp: inj_on_def)
- show "S = f ` (g ` S)"
- using g image_subset_iff by auto
- qed
- qed
-qed blast
-
subsection \<open>The set of natural numbers is infinite\<close>
lemma infinite_nat_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"