# 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>