--- a/src/HOL/Fun.thy Mon Oct 10 19:07:54 2022 +0200
+++ b/src/HOL/Fun.thy Tue Oct 11 10:45:42 2022 +0200
@@ -927,20 +927,6 @@
using that UNIV_I by (rule the_inv_into_f_f)
-subsection \<open>Cantor's Paradox\<close>
-
-theorem Cantors_paradox: "\<nexists>f. f ` A = Pow A"
-proof
- assume "\<exists>f. f ` A = Pow A"
- then obtain f where f: "f ` A = Pow A" ..
- let ?X = "{a \<in> A. a \<notin> f a}"
- have "?X \<in> Pow A" by blast
- then have "?X \<in> f ` A" by (simp only: f)
- then obtain x where "x \<in> A" and "f x = ?X" by blast
- then show False by blast
-qed
-
-
subsection \<open>Monotonicity\<close>
definition monotone_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
--- a/src/HOL/Set.thy Mon Oct 10 19:07:54 2022 +0200
+++ b/src/HOL/Set.thy Tue Oct 11 10:45:42 2022 +0200
@@ -952,6 +952,16 @@
lemma image_add_0 [simp]: "(+) (0::'a::comm_monoid_add) ` S = S"
by auto
+theorem Cantors_paradox: "\<nexists>f. f ` A = Pow A"
+proof
+ assume "\<exists>f. f ` A = Pow A"
+ then obtain f where f: "f ` A = Pow A" ..
+ let ?X = "{a \<in> A. a \<notin> f a}"
+ have "?X \<in> Pow A" by blast
+ then have "?X \<in> f ` A" by (simp only: f)
+ then obtain x where "x \<in> A" and "f x = ?X" by blast
+ then show False by blast
+qed
text \<open>\<^medskip> Range of a function -- just an abbreviation for image!\<close>