# HG changeset patch
# User nipkow
# Date 1665477942 -7200
# Node ID d1c26efb7a47f35c19922b6d6ab7cb69a3c3c4d5
# Parent  207b6fcfc47df9b0b74a76016783df414542fd33
moved theorem from Fun to Set

diff -r 207b6fcfc47d -r d1c26efb7a47 src/HOL/Fun.thy
--- 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"
diff -r 207b6fcfc47d -r d1c26efb7a47 src/HOL/Set.thy
--- 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>