Quelle Zorn_Lemma.thy Sprache: 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 "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

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.