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

src/HOL/Real/HahnBanach/ZornLemma.thy

author | wenzelm |

Mon, 21 Feb 2000 14:10:21 +0100 | |

changeset 8272 | 1329173b56ed |

parent 8104 | d9b3a224c0e6 |

child 8280 | 259073d16f84 |

permissions | -rw-r--r-- |

tuned footnote;

(* Title: HOL/Real/HahnBanach/ZornLemma.thy ID: $Id$ Author: Gertrud Bauer, TU Munich *) header {* Zorn's Lemma *}; 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$. *}; theorem Zorn's_Lemma: "(!!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 \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *}; assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S"; assume aS: "a:S"; show "ALL c:chain S. EX y:S. ALL z:c. z <= y"; proof; fix c; assume "c:chain S"; show "EX y:S. ALL z:c. z <= y"; proof (rule case_split); txt{* If $c$ is an empty chain, then every element in $S$ is an upper bound of $c$. *}; assume "c={}"; with aS; show ?thesis; by fast; txt{* If $c$ is non-empty, then $\Union c$ is an upper bound of $c$, lying in $S$. *}; next; assume c: "c~={}"; show ?thesis; proof; show "ALL z:c. z <= Union c"; by fast; show "Union c : S"; proof (rule r); from c; show "EX x. x:c"; by fast; qed; qed; qed; qed; qed; end;