src/HOL/SupInf.thy
changeset 33271 7be66dee1a5a
parent 33269 3b7e2dbbd684
child 33609 059cd49e4b1e
     1.1 --- a/src/HOL/SupInf.thy	Tue Oct 27 14:46:03 2009 +0000
     1.2 +++ b/src/HOL/SupInf.thy	Wed Oct 28 11:42:31 2009 +0000
     1.3 @@ -361,11 +361,6 @@
     1.4    shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
     1.5  by auto (metis Inf_insert_nonempty z) 
     1.6  
     1.7 -text{*We could prove the analogous result for the supremum, and also generalise it to the union operator.*}
     1.8 -lemma Inf_binary:
     1.9 -  "Inf{a, b::real} = min a b"
    1.10 -  by (subst Inf_insert_nonempty, auto)
    1.11 -
    1.12  lemma Inf_greater:
    1.13    fixes z :: real
    1.14    shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
    1.15 @@ -437,7 +432,7 @@
    1.16      by (simp add: Inf_real_def)
    1.17  qed
    1.18  
    1.19 -subsection{*Relate max and min to sup and inf.*}
    1.20 +subsection{*Relate max and min to Sup and Inf.*}
    1.21  
    1.22  lemma real_max_Sup:
    1.23    fixes x :: real