equal
deleted
inserted
replaced
773 by (rule the_inv_into_f_f) |
773 by (rule the_inv_into_f_f) |
774 |
774 |
775 |
775 |
776 subsection {* Cantor's Paradox *} |
776 subsection {* Cantor's Paradox *} |
777 |
777 |
778 lemma Cantors_paradox [no_atp]: |
778 lemma Cantors_paradox: |
779 "\<not>(\<exists>f. f ` A = Pow A)" |
779 "\<not>(\<exists>f. f ` A = Pow A)" |
780 proof clarify |
780 proof clarify |
781 fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast |
781 fix f assume "f ` A = Pow A" hence *: "Pow A \<le> f ` A" by blast |
782 let ?X = "{a \<in> A. a \<notin> f a}" |
782 let ?X = "{a \<in> A. a \<notin> f a}" |
783 have "?X \<in> Pow A" unfolding Pow_def by auto |
783 have "?X \<in> Pow A" unfolding Pow_def by auto |