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

src/HOL/Real/HahnBanach/ZornLemma.thy

author | wenzelm |

Tue Jul 15 19:39:37 2008 +0200 (2008-07-15) | |

changeset 27612 | d3eb431db035 |

parent 23378 | 1d138d6bb461 |

child 29234 | 60f7fb56f8cd |

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

modernized specifications and proofs;

tuned document;

tuned document;

1 (* Title: HOL/Real/HahnBanach/ZornLemma.thy

2 ID: $Id$

3 Author: Gertrud Bauer, TU Munich

4 *)

6 header {* Zorn's Lemma *}

8 theory ZornLemma

9 imports Zorn

10 begin

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 *}

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

34 txt {* If @{text c} is an empty chain, then every element in

35 @{text S} is an upper bound of @{text c}. *}

37 assume "c = {}"

38 with aS show ?thesis by fast

40 txt {* If @{text c} is non-empty, then @{text "\<Union>c"} is an upper

41 bound of @{text c}, lying in @{text S}. *}

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

58 end