src/HOL/Real/HahnBanach/ZornLemma.thy
changeset 8272 1329173b56ed
parent 8104 d9b3a224c0e6
child 8280 259073d16f84
equal deleted inserted replaced
8271:7602b57ba028 8272:1329173b56ed
    18 theorem Zorn's_Lemma: 
    18 theorem Zorn's_Lemma: 
    19   "(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S
    19   "(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S
    20   ==>  EX y: S. ALL z: S. y <= z --> y = z";
    20   ==>  EX y: S. ALL z: S. y <= z --> y = z";
    21 proof (rule Zorn_Lemma2);
    21 proof (rule Zorn_Lemma2);
    22   txt_raw {* \footnote{See
    22   txt_raw {* \footnote{See
    23   \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}}*};
    23   \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *};
    24   assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
    24   assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
    25   assume aS: "a:S";
    25   assume aS: "a:S";
    26   show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
    26   show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
    27   proof;
    27   proof;
    28     fix c; assume "c:chain S"; 
    28     fix c; assume "c:chain S";