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