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{}} \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";
    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$. *};

      assume c: "c~={}";
      show ?thesis; 
        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;