equal
deleted
inserted
replaced
768 shows "the_inv f (f x) = x" using assms UNIV_I |
768 shows "the_inv f (f x) = x" using assms UNIV_I |
769 by (rule the_inv_into_f_f) |
769 by (rule the_inv_into_f_f) |
770 |
770 |
771 subsection {* Cantor's Paradox *} |
771 subsection {* Cantor's Paradox *} |
772 |
772 |
773 lemma Cantors_paradox: |
773 lemma Cantors_paradox [no_atp]: |
774 "\<not>(\<exists>f. f ` A = Pow A)" |
774 "\<not>(\<exists>f. f ` A = Pow A)" |
775 proof clarify |
775 proof clarify |
776 fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast |
776 fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast |
777 let ?X = "{a \<in> A. a \<notin> f a}" |
777 let ?X = "{a \<in> A. a \<notin> f a}" |
778 have "?X \<in> Pow A" unfolding Pow_def by auto |
778 have "?X \<in> Pow A" unfolding Pow_def by auto |