7917
|
1 |
(* Title: HOL/Real/HahnBanach/ZornLemma.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gertrud Bauer, TU Munich
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* Zorn's Lemma *};
|
|
7 |
|
|
8 |
theory ZornLemma = Aux + Zorn:;
|
|
9 |
|
8104
|
10 |
text {* Zorn's Lemmas states: if every linear ordered subset of an
|
|
11 |
ordered set $S$ has an upper bound in $S$, then there exists a maximal
|
|
12 |
element in $S$. In our application, $S$ is a set of sets ordered by
|
|
13 |
set inclusion. Since the union of a chain of sets is an upper bound
|
|
14 |
for all elements of the chain, the conditions of Zorn's lemma can be
|
|
15 |
modified: if $S$ is non-empty, it suffices to show that for every
|
|
16 |
non-empty chain $c$ in $S$ the union of $c$ also lies in $S$. *};
|
7917
|
17 |
|
|
18 |
theorem Zorn's_Lemma:
|
8104
|
19 |
"(!!c. c: chain S ==> EX x. x:c ==> Union c : S) ==> a:S
|
7917
|
20 |
==> EX y: S. ALL z: S. y <= z --> y = z";
|
|
21 |
proof (rule Zorn_Lemma2);
|
8104
|
22 |
txt_raw {* \footnote{See
|
8272
|
23 |
\url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *};
|
8104
|
24 |
assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
|
7917
|
25 |
assume aS: "a:S";
|
|
26 |
show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
|
|
27 |
proof;
|
|
28 |
fix c; assume "c:chain S";
|
|
29 |
show "EX y:S. ALL z:c. z <= y";
|
|
30 |
proof (rule case_split);
|
|
31 |
|
|
32 |
txt{* If $c$ is an empty chain, then every element
|
7978
|
33 |
in $S$ is an upper bound of $c$. *};
|
7917
|
34 |
|
|
35 |
assume "c={}";
|
|
36 |
with aS; show ?thesis; by fast;
|
|
37 |
|
7927
|
38 |
txt{* If $c$ is non-empty, then $\Union c$
|
7978
|
39 |
is an upper bound of $c$, lying in $S$. *};
|
7917
|
40 |
|
|
41 |
next;
|
|
42 |
assume c: "c~={}";
|
|
43 |
show ?thesis;
|
|
44 |
proof;
|
|
45 |
show "ALL z:c. z <= Union c"; by fast;
|
|
46 |
show "Union c : S";
|
|
47 |
proof (rule r);
|
|
48 |
from c; show "EX x. x:c"; by fast;
|
|
49 |
qed;
|
|
50 |
qed;
|
|
51 |
qed;
|
|
52 |
qed;
|
|
53 |
qed;
|
|
54 |
|
|
55 |
end;
|