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 |
|
|
10 |
text{*
|
|
11 |
Zorn's Lemmas says: if every linear ordered subset of an ordered set
|
|
12 |
$S$ has an upper bound in $S$, then there exists a maximal element in $S$.
|
|
13 |
In our application $S$ is a set of sets, ordered by set inclusion. Since
|
|
14 |
the union of a chain of sets is an upperbound for all elements of the
|
|
15 |
chain, the conditions of Zorn's lemma can be modified:
|
|
16 |
If $S$ is non-empty, it suffices to show that for every non-empty
|
|
17 |
chain $c$ in $S$ the union of $c$ also lies in $S$:
|
|
18 |
*};
|
|
19 |
|
|
20 |
theorem Zorn's_Lemma:
|
|
21 |
"a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S)
|
|
22 |
==> EX y: S. ALL z: S. y <= z --> y = z";
|
|
23 |
proof (rule Zorn_Lemma2);
|
|
24 |
assume aS: "a:S";
|
|
25 |
assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : 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
|
|
33 |
in $S$ is an upperbound of $c$. *};
|
|
34 |
|
|
35 |
assume "c={}";
|
|
36 |
with aS; show ?thesis; by fast;
|
|
37 |
|
|
38 |
txt{* If $c$ is non-empty, then $\cup\; c$
|
|
39 |
is an upperbound of $c$, that lies in $S$. *};
|
|
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;
|