src/HOL/Real/HahnBanach/ZornLemma.thy
 changeset 8104 d9b3a224c0e6 parent 7978 1b99ee57d131 child 8272 1329173b56ed
```--- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Wed Jan 05 12:01:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Wed Jan 05 12:02:24 2000 +0100
@@ -7,24 +7,22 @@

theory ZornLemma = Aux + Zorn:;

-text{*
-Zorn's Lemmas states: if every linear ordered subset of an ordered set
-\$S\$ has an upper bound in \$S\$, then there exists a maximal element in \$S\$.
-In our application, \$S\$ is a set of sets ordered by set inclusion. Since
-the union of a chain of sets is an upper bound for all elements of the
-chain, the conditions of Zorn's lemma can be modified:
-if \$S\$ is non-empty, it suffices to show that for every non-empty
-chain \$c\$ in \$S\$ the union of \$c\$ also lies in \$S\$.
-*};
+text {* Zorn's Lemmas states: if every linear ordered subset of an
+ordered set \$S\$ has an upper bound in \$S\$, then there exists a maximal
+element in \$S\$.  In our application, \$S\$ is a set of sets ordered by
+set inclusion. Since the union of a chain of sets is an upper bound
+for all elements of the chain, the conditions of Zorn's lemma can be
+modified: if \$S\$ is non-empty, it suffices to show that for every
+non-empty chain \$c\$ in \$S\$ the union of \$c\$ also lies in \$S\$. *};

theorem Zorn's_Lemma:
-  "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S)
+  "(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S
==>  EX y: S. ALL z: S. y <= z --> y = z";
proof (rule Zorn_Lemma2);
-  txt_raw{* \footnote{See
+  txt_raw {* \footnote{See
\url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}}*};
+  assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
assume aS: "a:S";
-  assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
proof;
fix c; assume "c:chain S"; ```