Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Bounds.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Hahn_Banach/Bounds.thy
    Author:     Gertrud Bauer, TU Munich
*)

section \<open>Bounds\<close>

theory Bounds
imports Main "HOL-Analysis.Continuum_Not_Denumerable"
begin

locale lub =
  fixes A and x
  assumes least [intro?]: "(\a. a \ A \ a \ b) \ x \ b"
    and upper [intro?]: "a \ A \ a \ x"

lemmas [elim?] = lub.least lub.upper

definition the_lub :: "'a::order set \ 'a" ("\_" [90] 90)
  where "the_lub A = The (lub A)"

lemma the_lub_equality [elim?]:
  assumes "lub A x"
  shows "\A = (x::'a::order)"
proof -
  interpret lub A x by fact
  show ?thesis
  proof (unfold the_lub_def)
    from \<open>lub A x\<close> show "The (lub A) = x"
    proof
      fix x' assume lub': "lub A x'"
      show "x' = x"
      proof (rule order_antisym)
        from lub' show "x' \<le> x"
        proof
          fix a assume "a \ A"
          then show "a \ x" ..
        qed
        show "x \ x'"
        proof
          fix a assume "a \ A"
          with lub' show "a \ x'" ..
        qed
      qed
    qed
  qed
qed

lemma the_lubI_ex:
  assumes ex: "\x. lub A x"
  shows "lub A (\A)"
proof -
  from ex obtain x where x: "lub A x" ..
  also from x have [symmetric]: "\A = x" ..
  finally show ?thesis .
qed

lemma real_complete: "\a::real. a \ A \ \y. \a \ A. a \ y \ \x. lub A x"
  by (intro exI[of _ "Sup A"]) (auto intro!: cSup_upper cSup_least simp: lub_def)

end

¤ Dauer der Verarbeitung: 0.13 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.