summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Isar_examples/Cantor.thy

changeset 7800 | 8ee919e42174 |

parent 7748 | 5b9c45b21782 |

child 7819 | 6dd018b6cf3f |

--- a/src/HOL/Isar_examples/Cantor.thy Fri Oct 08 15:08:47 1999 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Fri Oct 08 15:09:14 1999 +0200 @@ -6,15 +6,16 @@ chapter of "Isabelle's Object-Logics" (Larry Paulson). *) -header {* More classical proofs: Cantor's Theorem *}; +header {* Cantor's Theorem *}; theory Cantor = Main:; text {* Cantor's Theorem states that every set has more subsets than it has - elements. It has become a favourite basic example in higher-order logic - since it is so easily expressed: \[\all{f::\alpha \To \alpha \To \idt{bool}} - \ex{S::\alpha \To \idt{bool}} \all{x::\alpha}. f \ap x \not= S\] + elements. It has become a favorite basic example in pure + higher-order logic since it is so easily expressed: \[\all{f::\alpha + \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}} + \all{x::\alpha}. f \ap x \not= S\] Viewing types as sets, $\alpha \To \idt{bool}$ represents the powerset of $\alpha$. This version of the theorem states that for every function from