summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Hahn_Banach/Zorn_Lemma.thy

author | paulson <lp15@cam.ac.uk> |

Mon May 23 15:33:24 2016 +0100 (2016-05-23) | |

changeset 63114 | 27afe7af7379 |

parent 61879 | e4f9d8f094fe |

permissions | -rw-r--r-- |

Lots of new material for multivariate analysis

1 (* Title: HOL/Hahn_Banach/Zorn_Lemma.thy

2 Author: Gertrud Bauer, TU Munich

3 *)

5 section \<open>Zorn's Lemma\<close>

7 theory Zorn_Lemma

8 imports Main

9 begin

11 text \<open>

12 Zorn's Lemmas states: if every linear ordered subset of an ordered set \<open>S\<close>

13 has an upper bound in \<open>S\<close>, then there exists a maximal element in \<open>S\<close>. In

14 our application, \<open>S\<close> is a set of sets ordered by set inclusion. Since the

15 union of a chain of sets is an upper bound for all elements of the chain,

16 the conditions of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it

17 suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close>

18 also lies in \<open>S\<close>.

19 \<close>

21 theorem Zorn's_Lemma:

22 assumes r: "\<And>c. c \<in> chains S \<Longrightarrow> \<exists>x. x \<in> c \<Longrightarrow> \<Union>c \<in> S"

23 and aS: "a \<in> S"

24 shows "\<exists>y \<in> S. \<forall>z \<in> S. y \<subseteq> z \<longrightarrow> z = y"

25 proof (rule Zorn_Lemma2)

26 show "\<forall>c \<in> chains S. \<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"

27 proof

28 fix c assume "c \<in> chains S"

29 show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"

30 proof cases

31 txt \<open>If \<open>c\<close> is an empty chain, then every element in \<open>S\<close> is an upper

32 bound of \<open>c\<close>.\<close>

34 assume "c = {}"

35 with aS show ?thesis by fast

37 txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper bound of \<open>c\<close>, lying in

38 \<open>S\<close>.\<close>

39 next

40 assume "c \<noteq> {}"

41 show ?thesis

42 proof

43 show "\<forall>z \<in> c. z \<subseteq> \<Union>c" by fast

44 show "\<Union>c \<in> S"

45 proof (rule r)

46 from \<open>c \<noteq> {}\<close> show "\<exists>x. x \<in> c" by fast

47 show "c \<in> chains S" by fact

48 qed

49 qed

50 qed

51 qed

52 qed

54 end