summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 20 Jun 2016 17:25:08 +0200 | |

changeset 63323 | 814541a57d89 |

parent 63322 | bc1f17d45e91 |

child 63324 | 1e98146f3581 |

tuned proof;

src/HOL/Fun.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Fun.thy Mon Jun 20 17:03:50 2016 +0200 +++ b/src/HOL/Fun.thy Mon Jun 20 17:25:08 2016 +0200 @@ -793,15 +793,15 @@ subsection \<open>Cantor's Paradox\<close> -lemma Cantors_paradox: "\<not> (\<exists>f. f ` A = Pow A)" -proof clarify - fix f - assume "f ` A = Pow A" - then have *: "Pow A \<subseteq> f ` A" by blast +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" unfolding Pow_def by auto - with * obtain x where "x \<in> A \<and> f x = ?X" by blast - then show False by best + 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