src/HOL/Real/HahnBanach/Bounds.thy
changeset 7566 c5a3f980a7af
parent 7535 599d3414b51d
child 7656 2f18c0ffc348
     1.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Tue Sep 21 17:30:55 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Tue Sep 21 17:31:20 1999 +0200
     1.3 @@ -1,3 +1,7 @@
     1.4 +(*  Title:      HOL/Real/HahnBanach/Bounds.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Gertrud Bauer, TU Munich
     1.7 +*)
     1.8  
     1.9  theory Bounds = Main + Real:;
    1.10  
    1.11 @@ -60,8 +64,6 @@
    1.12    is_Sup :: "('a::order) set => 'a set => 'a => bool"
    1.13    "is_Sup A B x == isLub A B x"
    1.14     
    1.15 -  (* was:  x:A & is_Least (UpperBounds A B) x" *)
    1.16 -
    1.17    Sup :: "('a::order) set => 'a set => 'a"
    1.18    "Sup A B == Eps (is_Sup A B)"
    1.19  
    1.20 @@ -84,9 +86,6 @@
    1.21    "INF x. P" == "INF x:UNIV. P";
    1.22  
    1.23  
    1.24 -lemma [intro]: "[| x:A; !!y. y:B ==> y <= x |] ==> x: UpperBounds A B";
    1.25 -  by (unfold UpperBounds_def is_UpperBound_def) force;
    1.26 -
    1.27  lemma ub_ge_sup: "isUb A B y ==> is_Sup A B s ==> s <= y";
    1.28    by (unfold is_Sup_def, rule isLub_le_isUb);
    1.29