(* 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 toshow 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 "c = {}") 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> case True with aS show ?thesis by fast next 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> case False 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.0 Sekunden
(vorverarbeitet)
¤
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.
