|
1 (* Title: HOL/Hahn_Banach/Zorn_Lemma.thy |
|
2 Author: Gertrud Bauer, TU Munich |
|
3 *) |
|
4 |
|
5 header {* Zorn's Lemma *} |
|
6 |
|
7 theory Zorn_Lemma |
|
8 imports Zorn |
|
9 begin |
|
10 |
|
11 text {* |
|
12 Zorn's Lemmas states: if every linear ordered subset of an ordered |
|
13 set @{text S} has an upper bound in @{text S}, then there exists a |
|
14 maximal element in @{text S}. In our application, @{text S} is a |
|
15 set of sets ordered by set inclusion. Since the union of a chain of |
|
16 sets is an upper bound for all elements of the chain, the conditions |
|
17 of Zorn's lemma can be modified: if @{text S} is non-empty, it |
|
18 suffices to show that for every non-empty chain @{text c} in @{text |
|
19 S} the union of @{text c} also lies in @{text S}. |
|
20 *} |
|
21 |
|
22 theorem Zorn's_Lemma: |
|
23 assumes r: "\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S" |
|
24 and aS: "a \<in> S" |
|
25 shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z" |
|
26 proof (rule Zorn_Lemma2) |
|
27 show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
|
28 proof |
|
29 fix c assume "c \<in> chain S" |
|
30 show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
|
31 proof cases |
|
32 |
|
33 txt {* If @{text c} is an empty chain, then every element in |
|
34 @{text S} is an upper bound of @{text c}. *} |
|
35 |
|
36 assume "c = {}" |
|
37 with aS show ?thesis by fast |
|
38 |
|
39 txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper |
|
40 bound of @{text c}, lying in @{text S}. *} |
|
41 |
|
42 next |
|
43 assume "c \<noteq> {}" |
|
44 show ?thesis |
|
45 proof |
|
46 show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast |
|
47 show "\<Union>c \<in> S" |
|
48 proof (rule r) |
|
49 from `c \<noteq> {}` show "\<exists>x. x \<in> c" by fast |
|
50 show "c \<in> chain S" by fact |
|
51 qed |
|
52 qed |
|
53 qed |
|
54 qed |
|
55 qed |
|
56 |
|
57 end |