Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Zorn_Lemma.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.