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