src/HOL/SupInf.thy
 author paulson Tue Oct 27 12:59:57 2009 +0000 (2009-10-27) changeset 33269 3b7e2dbbd684 child 33271 7be66dee1a5a permissions -rw-r--r--
New theory SupInf of the supremum and infimum operators for sets of reals.
```     1 (*  Author: Amine Chaieb and L C Paulson, University of Cambridge *)
```
```     2
```
```     3 header {*Sup and Inf Operators on Sets of Reals.*}
```
```     4
```
```     5 theory SupInf
```
```     6 imports RComplete
```
```     7 begin
```
```     8
```
```     9 lemma minus_max_eq_min:
```
```    10   fixes x :: "'a::{lordered_ab_group_add, linorder}"
```
```    11   shows "- (max x y) = min (-x) (-y)"
```
```    12 by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1)
```
```    13
```
```    14 lemma minus_min_eq_max:
```
```    15   fixes x :: "'a::{lordered_ab_group_add, linorder}"
```
```    16   shows "- (min x y) = max (-x) (-y)"
```
```    17 by (metis minus_max_eq_min minus_minus)
```
```    18
```
```    19 lemma minus_Max_eq_Min [simp]:
```
```    20   fixes S :: "'a::{lordered_ab_group_add, linorder} set"
```
```    21   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
```
```    22 proof (induct S rule: finite_ne_induct)
```
```    23   case (singleton x)
```
```    24   thus ?case by simp
```
```    25 next
```
```    26   case (insert x S)
```
```    27   thus ?case by (simp add: minus_max_eq_min)
```
```    28 qed
```
```    29
```
```    30 lemma minus_Min_eq_Max [simp]:
```
```    31   fixes S :: "'a::{lordered_ab_group_add, linorder} set"
```
```    32   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
```
```    33 proof (induct S rule: finite_ne_induct)
```
```    34   case (singleton x)
```
```    35   thus ?case by simp
```
```    36 next
```
```    37   case (insert x S)
```
```    38   thus ?case by (simp add: minus_min_eq_max)
```
```    39 qed
```
```    40
```
```    41 instantiation real :: Sup
```
```    42 begin
```
```    43 definition
```
```    44   Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
```
```    45
```
```    46 instance ..
```
```    47 end
```
```    48
```
```    49 instantiation real :: Inf
```
```    50 begin
```
```    51 definition
```
```    52   Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))"
```
```    53
```
```    54 instance ..
```
```    55 end
```
```    56
```
```    57 subsection{*Supremum of a set of reals*}
```
```    58
```
```    59 lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*)
```
```    60   fixes x :: real
```
```    61   assumes x: "x \<in> X"
```
```    62       and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
```
```    63   shows "x \<le> Sup X"
```
```    64 proof (auto simp add: Sup_real_def)
```
```    65   from reals_complete2
```
```    66   obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
```
```    67     by (blast intro: x z)
```
```    68   hence "x \<le> s"
```
```    69     by (blast intro: x z)
```
```    70   also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
```
```    71     by (fast intro: Least_equality [symmetric])
```
```    72   finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
```
```    73 qed
```
```    74
```
```    75 lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*)
```
```    76   fixes z :: real
```
```    77   assumes x: "X \<noteq> {}"
```
```    78       and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
```
```    79   shows "Sup X \<le> z"
```
```    80 proof (auto simp add: Sup_real_def)
```
```    81   from reals_complete2 x
```
```    82   obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
```
```    83     by (blast intro: z)
```
```    84   hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
```
```    85     by (best intro: Least_equality)
```
```    86   also with s z have "... \<le> z"
```
```    87     by blast
```
```    88   finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
```
```    89 qed
```
```    90
```
```    91 lemma Sup_singleton [simp]: "Sup {x::real} = x"
```
```    92   by (force intro: Least_equality simp add: Sup_real_def)
```
```    93
```
```    94 lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
```
```    95   fixes z :: real
```
```    96   assumes X: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
```
```    97   shows  "Sup X = z"
```
```    98   by (force intro: Least_equality X z simp add: Sup_real_def)
```
```    99
```
```   100 lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
```
```   101   fixes x :: real
```
```   102   shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
```
```   103   by (metis Sup_upper real_le_trans)
```
```   104
```
```   105 lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
```
```   106   fixes z :: real
```
```   107   shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
```
```   108   by (metis Sup_least Sup_upper linorder_not_le le_less_trans)
```
```   109
```
```   110 lemma Sup_eq:
```
```   111   fixes a :: real
```
```   112   shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a)
```
```   113         \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
```
```   114   by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
```
```   115         insert_not_empty real_le_anti_sym)
```
```   116
```
```   117 lemma Sup_le:
```
```   118   fixes S :: "real set"
```
```   119   shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
```
```   120 by (metis SupInf.Sup_least setle_def)
```
```   121
```
```   122 lemma Sup_upper_EX:
```
```   123   fixes x :: real
```
```   124   shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow>  x \<le> Sup X"
```
```   125   by blast
```
```   126
```
```   127 lemma Sup_insert_nonempty:
```
```   128   fixes x :: real
```
```   129   assumes x: "x \<in> X"
```
```   130       and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
```
```   131   shows "Sup (insert a X) = max a (Sup X)"
```
```   132 proof (cases "Sup X \<le> a")
```
```   133   case True
```
```   134   thus ?thesis
```
```   135     apply (simp add: max_def)
```
```   136     apply (rule Sup_eq_maximum)
```
```   137     apply (metis insertCI)
```
```   138     apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)
```
```   139     done
```
```   140 next
```
```   141   case False
```
```   142   hence 1:"a < Sup X" by simp
```
```   143   have "Sup X \<le> Sup (insert a X)"
```
```   144     apply (rule Sup_least)
```
```   145     apply (metis empty_psubset_nonempty psubset_eq x)
```
```   146     apply (rule Sup_upper_EX)
```
```   147     apply blast
```
```   148     apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
```
```   149     done
```
```   150   moreover
```
```   151   have "Sup (insert a X) \<le> Sup X"
```
```   152     apply (rule Sup_least)
```
```   153     apply blast
```
```   154     apply (metis False Sup_upper insertE real_le_linear z)
```
```   155     done
```
```   156   ultimately have "Sup (insert a X) = Sup X"
```
```   157     by (blast intro:  antisym )
```
```   158   thus ?thesis
```
```   159     by (metis 1 min_max.le_iff_sup real_less_def)
```
```   160 qed
```
```   161
```
```   162 lemma Sup_insert_if:
```
```   163   fixes X :: "real set"
```
```   164   assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
```
```   165   shows "Sup (insert a X) = (if X={} then a else max a (Sup X))"
```
```   166 by auto (metis Sup_insert_nonempty z)
```
```   167
```
```   168 lemma Sup:
```
```   169   fixes S :: "real set"
```
```   170   shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
```
```   171 by  (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI)
```
```   172
```
```   173 lemma Sup_finite_Max:
```
```   174   fixes S :: "real set"
```
```   175   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   176   shows "Sup S = Max S"
```
```   177 using fS Se
```
```   178 proof-
```
```   179   let ?m = "Max S"
```
```   180   from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
```
```   181   with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def)
```
```   182   from Max_in[OF fS Se] lub have mrS: "?m \<le> Sup S"
```
```   183     by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
```
```   184   moreover
```
```   185   have "Sup S \<le> ?m" using Sm lub
```
```   186     by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
```
```   187   ultimately  show ?thesis by arith
```
```   188 qed
```
```   189
```
```   190 lemma Sup_finite_in:
```
```   191   fixes S :: "real set"
```
```   192   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   193   shows "Sup S \<in> S"
```
```   194   using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
```
```   195
```
```   196 lemma Sup_finite_ge_iff:
```
```   197   fixes S :: "real set"
```
```   198   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   199   shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
```
```   200 by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans)
```
```   201
```
```   202 lemma Sup_finite_le_iff:
```
```   203   fixes S :: "real set"
```
```   204   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   205   shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
```
```   206 by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans)
```
```   207
```
```   208 lemma Sup_finite_gt_iff:
```
```   209   fixes S :: "real set"
```
```   210   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   211   shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
```
```   212 by (metis Se Sup_finite_le_iff fS linorder_not_less)
```
```   213
```
```   214 lemma Sup_finite_lt_iff:
```
```   215   fixes S :: "real set"
```
```   216   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   217   shows "a > Sup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
```
```   218 by (metis Se Sup_finite_ge_iff fS linorder_not_less)
```
```   219
```
```   220 lemma Sup_unique:
```
```   221   fixes S :: "real set"
```
```   222   shows "S *<= b \<Longrightarrow> (\<forall>b' < b. \<exists>x \<in> S. b' < x) \<Longrightarrow> Sup S = b"
```
```   223 unfolding setle_def
```
```   224 apply (rule Sup_eq, auto)
```
```   225 apply (metis linorder_not_less)
```
```   226 done
```
```   227
```
```   228 lemma Sup_abs_le:
```
```   229   fixes S :: "real set"
```
```   230   shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
```
```   231 by (auto simp add: abs_le_interval_iff) (metis Sup_upper2)
```
```   232
```
```   233 lemma Sup_bounds:
```
```   234   fixes S :: "real set"
```
```   235   assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
```
```   236   shows "a \<le> Sup S \<and> Sup S \<le> b"
```
```   237 proof-
```
```   238   from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
```
```   239   hence b: "Sup S \<le> b" using u
```
```   240     by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
```
```   241   from Se obtain y where y: "y \<in> S" by blast
```
```   242   from lub l have "a \<le> Sup S"
```
```   243     by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
```
```   244        (metis le_iff_sup le_sup_iff y)
```
```   245   with b show ?thesis by blast
```
```   246 qed
```
```   247
```
```   248 lemma Sup_asclose:
```
```   249   fixes S :: "real set"
```
```   250   assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
```
```   251 proof-
```
```   252   have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
```
```   253   thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th
```
```   254     by  (auto simp add: setge_def setle_def)
```
```   255 qed
```
```   256
```
```   257
```
```   258 subsection{*Infimum of a set of reals*}
```
```   259
```
```   260 lemma Inf_lower [intro]:
```
```   261   fixes z :: real
```
```   262   assumes x: "x \<in> X"
```
```   263       and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
```
```   264   shows "Inf X \<le> x"
```
```   265 proof -
```
```   266   have "-x \<le> Sup (uminus ` X)"
```
```   267     by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z)
```
```   268   thus ?thesis
```
```   269     by (auto simp add: Inf_real_def)
```
```   270 qed
```
```   271
```
```   272 lemma Inf_greatest [intro]:
```
```   273   fixes z :: real
```
```   274   assumes x: "X \<noteq> {}"
```
```   275       and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
```
```   276   shows "z \<le> Inf X"
```
```   277 proof -
```
```   278   have "Sup (uminus ` X) \<le> -z" using x z by (force intro: Sup_least)
```
```   279   hence "z \<le> - Sup (uminus ` X)"
```
```   280     by simp
```
```   281   thus ?thesis
```
```   282     by (auto simp add: Inf_real_def)
```
```   283 qed
```
```   284
```
```   285 lemma Inf_singleton [simp]: "Inf {x::real} = x"
```
```   286   by (simp add: Inf_real_def)
```
```   287
```
```   288 lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*)
```
```   289   fixes z :: real
```
```   290   assumes x: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
```
```   291   shows  "Inf X = z"
```
```   292 proof -
```
```   293   have "Sup (uminus ` X) = -z" using x z
```
```   294     by (force intro: Sup_eq_maximum x z)
```
```   295   thus ?thesis
```
```   296     by (simp add: Inf_real_def)
```
```   297 qed
```
```   298
```
```   299 lemma Inf_lower2:
```
```   300   fixes x :: real
```
```   301   shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
```
```   302   by (metis Inf_lower real_le_trans)
```
```   303
```
```   304 lemma Inf_real_iff:
```
```   305   fixes z :: real
```
```   306   shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
```
```   307   by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear
```
```   308             order_less_le_trans)
```
```   309
```
```   310 lemma Inf_eq:
```
```   311   fixes a :: real
```
```   312   shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
```
```   313   by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
```
```   314         insert_absorb insert_not_empty real_le_anti_sym)
```
```   315
```
```   316 lemma Inf_ge:
```
```   317   fixes S :: "real set"
```
```   318   shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
```
```   319 by (metis SupInf.Inf_greatest setge_def)
```
```   320
```
```   321 lemma Inf_lower_EX:
```
```   322   fixes x :: real
```
```   323   shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
```
```   324   by blast
```
```   325
```
```   326 lemma Inf_insert_nonempty:
```
```   327   fixes x :: real
```
```   328   assumes x: "x \<in> X"
```
```   329       and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
```
```   330   shows "Inf (insert a X) = min a (Inf X)"
```
```   331 proof (cases "a \<le> Inf X")
```
```   332   case True
```
```   333   thus ?thesis
```
```   334     by (simp add: min_def)
```
```   335        (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z)
```
```   336 next
```
```   337   case False
```
```   338   hence 1:"Inf X < a" by simp
```
```   339   have "Inf (insert a X) \<le> Inf X"
```
```   340     apply (rule Inf_greatest)
```
```   341     apply (metis empty_psubset_nonempty psubset_eq x)
```
```   342     apply (rule Inf_lower_EX)
```
```   343     apply (blast intro: elim:)
```
```   344     apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
```
```   345     done
```
```   346   moreover
```
```   347   have "Inf X \<le> Inf (insert a X)"
```
```   348     apply (rule Inf_greatest)
```
```   349     apply blast
```
```   350     apply (metis False Inf_lower insertE real_le_linear z)
```
```   351     done
```
```   352   ultimately have "Inf (insert a X) = Inf X"
```
```   353     by (blast intro:  antisym )
```
```   354   thus ?thesis
```
```   355     by (metis False min_max.inf_absorb2 real_le_linear)
```
```   356 qed
```
```   357
```
```   358 lemma Inf_insert_if:
```
```   359   fixes X :: "real set"
```
```   360   assumes z:  "!!x. x \<in> X \<Longrightarrow> z \<le> x"
```
```   361   shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
```
```   362 by auto (metis Inf_insert_nonempty z)
```
```   363
```
```   364 text{*We could prove the analogous result for the supremum, and also generalise it to the union operator.*}
```
```   365 lemma Inf_binary:
```
```   366   "Inf{a, b::real} = min a b"
```
```   367   by (subst Inf_insert_nonempty, auto)
```
```   368
```
```   369 lemma Inf_greater:
```
```   370   fixes z :: real
```
```   371   shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
```
```   372   by (metis Inf_real_iff mem_def not_leE)
```
```   373
```
```   374 lemma Inf_close:
```
```   375   fixes e :: real
```
```   376   shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
```
```   377   by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict)
```
```   378
```
```   379 lemma Inf_finite_Min:
```
```   380   fixes S :: "real set"
```
```   381   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S"
```
```   382 by (simp add: Inf_real_def Sup_finite_Max image_image)
```
```   383
```
```   384 lemma Inf_finite_in:
```
```   385   fixes S :: "real set"
```
```   386   assumes fS: "finite S" and Se: "S \<noteq> {}"
```
```   387   shows "Inf S \<in> S"
```
```   388   using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
```
```   389
```
```   390 lemma Inf_finite_ge_iff:
```
```   391   fixes S :: "real set"
```
```   392   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
```
```   393 by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans)
```
```   394
```
```   395 lemma Inf_finite_le_iff:
```
```   396   fixes S :: "real set"
```
```   397   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
```
```   398 by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
```
```   399           real_le_anti_sym real_le_linear)
```
```   400
```
```   401 lemma Inf_finite_gt_iff:
```
```   402   fixes S :: "real set"
```
```   403   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
```
```   404 by (metis Inf_finite_le_iff linorder_not_less)
```
```   405
```
```   406 lemma Inf_finite_lt_iff:
```
```   407   fixes S :: "real set"
```
```   408   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
```
```   409 by (metis Inf_finite_ge_iff linorder_not_less)
```
```   410
```
```   411 lemma Inf_unique:
```
```   412   fixes S :: "real set"
```
```   413   shows "b <=* S \<Longrightarrow> (\<forall>b' > b. \<exists>x \<in> S. b' > x) \<Longrightarrow> Inf S = b"
```
```   414 unfolding setge_def
```
```   415 apply (rule Inf_eq, auto)
```
```   416 apply (metis less_le_not_le linorder_not_less)
```
```   417 done
```
```   418
```
```   419 lemma Inf_abs_ge:
```
```   420   fixes S :: "real set"
```
```   421   shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
```
```   422 by (simp add: Inf_real_def) (rule Sup_abs_le, auto)
```
```   423
```
```   424 lemma Inf_asclose:
```
```   425   fixes S :: "real set"
```
```   426   assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
```
```   427 proof -
```
```   428   have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
```
```   429     by auto
```
```   430   also have "... \<le> e"
```
```   431     apply (rule Sup_asclose)
```
```   432     apply (auto simp add: S)
```
```   433     apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def)
```
```   434     done
```
```   435   finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
```
```   436   thus ?thesis
```
```   437     by (simp add: Inf_real_def)
```
```   438 qed
```
```   439
```
```   440 subsection{*Relate max and min to sup and inf.*}
```
```   441
```
```   442 lemma real_max_Sup:
```
```   443   fixes x :: real
```
```   444   shows "max x y = Sup {x,y}"
```
```   445 proof-
```
```   446   have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
```
```   447   from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \<le> max x y" by simp
```
```   448   moreover
```
```   449   have "max x y \<le> Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"]
```
```   450     by (simp add: linorder_linear)
```
```   451   ultimately show ?thesis by arith
```
```   452 qed
```
```   453
```
```   454 lemma real_min_Inf:
```
```   455   fixes x :: real
```
```   456   shows "min x y = Inf {x,y}"
```
```   457 proof-
```
```   458   have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
```
```   459   from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \<le> min x y"
```
```   460     by (simp add: linorder_linear)
```
```   461   moreover
```
```   462   have "min x y \<le> Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"]
```
```   463     by simp
```
```   464   ultimately show ?thesis by arith
```
```   465 qed
```
```   466
```
```   467 end
```