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

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";