1(* Title: HOL/Hahn_Banach/Bounds.thy 2 Author: Gertrud Bauer, TU Munich 3*) 4 5section \<open>Bounds\<close> 6 7theory Bounds 8imports Main "HOL-Analysis.Continuum_Not_Denumerable" 9begin 10 11locale lub = 12 fixes A and x 13 assumes least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<le> b) \<Longrightarrow> x \<le> b" 14 and upper [intro?]: "a \<in> A \<Longrightarrow> a \<le> x" 15 16lemmas [elim?] = lub.least lub.upper 17 18definition the_lub :: "'a::order set \<Rightarrow> 'a" ("\<Squnion>_" [90] 90) 19 where "the_lub A = The (lub A)" 20 21lemma the_lub_equality [elim?]: 22 assumes "lub A x" 23 shows "\<Squnion>A = (x::'a::order)" 24proof - 25 interpret lub A x by fact 26 show ?thesis 27 proof (unfold the_lub_def) 28 from \<open>lub A x\<close> show "The (lub A) = x" 29 proof 30 fix x' assume lub': "lub A x'" 31 show "x' = x" 32 proof (rule order_antisym) 33 from lub' show "x' \<le> x" 34 proof 35 fix a assume "a \<in> A" 36 then show "a \<le> x" .. 37 qed 38 show "x \<le> x'" 39 proof 40 fix a assume "a \<in> A" 41 with lub' show "a \<le> x'" .. 42 qed 43 qed 44 qed 45 qed 46qed 47 48lemma the_lubI_ex: 49 assumes ex: "\<exists>x. lub A x" 50 shows "lub A (\<Squnion>A)" 51proof - 52 from ex obtain x where x: "lub A x" .. 53 also from x have [symmetric]: "\<Squnion>A = x" .. 54 finally show ?thesis . 55qed 56 57lemma real_complete: "\<exists>a::real. a \<in> A \<Longrightarrow> \<exists>y. \<forall>a \<in> A. a \<le> y \<Longrightarrow> \<exists>x. lub A x" 58 by (intro exI[of _ "Sup A"]) (auto intro!: cSup_upper cSup_least simp: lub_def) 59 60end 61