(* 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" thenshow"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" .. alsofrom x have [symmetric]: "\A = x" .. finallyshow ?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.11 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.
