17 suffices to show that for every non-empty chain @{text c} in @{text |
17 suffices to show that for every non-empty chain @{text c} in @{text |
18 S} the union of @{text c} also lies in @{text S}. |
18 S} the union of @{text c} also lies in @{text S}. |
19 *} |
19 *} |
20 |
20 |
21 theorem Zorn's_Lemma: |
21 theorem Zorn's_Lemma: |
22 "(\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S) \<Longrightarrow> a \<in> S |
22 assumes r: "\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S" |
23 \<Longrightarrow> \<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z" |
23 and aS: "a \<in> S" |
|
24 shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> y = z" |
24 proof (rule Zorn_Lemma2) |
25 proof (rule Zorn_Lemma2) |
25 txt_raw {* \footnote{See |
26 txt_raw {* \footnote{See |
26 \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *} |
27 \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}} \isanewline *} |
27 assume r: "\<And>c. c \<in> chain S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S" |
|
28 assume aS: "a \<in> S" |
|
29 show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
28 show "\<forall>c \<in> chain S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
30 proof |
29 proof |
31 fix c assume "c \<in> chain S" |
30 fix c assume "c \<in> chain S" |
32 show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
31 show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y" |
33 proof cases |
32 proof cases |
34 |
33 |
35 txt {* If @{text c} is an empty chain, then every element in |
34 txt {* If @{text c} is an empty chain, then every element in |
36 @{text S} is an upper bound of @{text c}. *} |
35 @{text S} is an upper bound of @{text c}. *} |
37 |
36 |
38 assume "c = {}" |
37 assume "c = {}" |
39 with aS show ?thesis by fast |
38 with aS show ?thesis by fast |
40 |
39 |
41 txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper |
40 txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper |
42 bound of @{text c}, lying in @{text S}. *} |
41 bound of @{text c}, lying in @{text S}. *} |
43 |
42 |
44 next |
43 next |
45 assume c: "c \<noteq> {}" |
44 assume c: "c \<noteq> {}" |
46 show ?thesis |
45 show ?thesis |
47 proof |
46 proof |
48 show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast |
47 show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast |
49 show "\<Union>c \<in> S" |
48 show "\<Union>c \<in> S" |
50 proof (rule r) |
49 proof (rule r) |
51 from c show "\<exists>x. x \<in> c" by fast |
50 from c show "\<exists>x. x \<in> c" by fast |
52 qed |
51 qed |
53 qed |
52 qed |
54 qed |
53 qed |
55 qed |
54 qed |
56 qed |
55 qed |