(* Title: HOL/Hahn_Banach/Zorn_Lemma.thy
Author: Gertrud Bauer, TU Munich
*)
section \<open>Zorn's Lemma\<close>
theory Zorn_Lemma
imports Main
begin
text \<open>
Zorn's Lemmas states: if every linear ordered subset of an ordered set \S\
has an upper bound in \<open>S\<close>, then there exists a maximal element in \<open>S\<close>. In
our application, \<open>S\<close> is a set of sets ordered by set inclusion. Since the
union of a chain of sets is an upper bound for all elements of the chain,
the conditions of Zorn's lemma can be modified: if \S\ is non-empty, it
suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close>
also lies in \<open>S\<close>.
\<close>
theorem Zorn's_Lemma:
assumes r: "\c. c \ chains S \ \x. x \ c \ \c \ S"
and aS: "a \ S"
shows "\y \ S. \z \ S. y \ z \ z = y"
proof (rule Zorn_Lemma2)
show "\c \ chains S. \y \ S. \z \ c. z \ y"
proof
fix c assume "c \ chains S"
show "\y \ S. \z \ c. z \ y"
proof cases
txt \<open>If \<open>c\<close> is an empty chain, then every element in \<open>S\<close> is an upper
bound of \<open>c\<close>.\<close>
assume "c = {}"
with aS show ?thesis by fast
txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper bound of \<open>c\<close>, lying in
\<open>S\<close>.\<close>
next
assume "c \ {}"
show ?thesis
proof
show "\z \ c. z \ \c" by fast
show "\c \ S"
proof (rule r)
from \<open>c \<noteq> {}\<close> show "\<exists>x. x \<in> c" by fast
show "c \ chains S" by fact
qed
qed
qed
qed
qed
end
¤ Dauer der Verarbeitung: 0.8 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
