src/HOL/Real/HahnBanach/ZornLemma.thy
 changeset 8272 1329173b56ed parent 8104 d9b3a224c0e6 child 8280 259073d16f84
equal 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"; `