| changeset 7656 | 2f18c0ffc348 |
| parent 7566 | c5a3f980a7af |
| child 7808 | fd019ac3485f |
--- a/src/HOL/Real/HahnBanach/Bounds.thy Wed Sep 29 15:35:09 1999 +0200 +++ b/src/HOL/Real/HahnBanach/Bounds.thy Wed Sep 29 16:41:52 1999 +0200 @@ -86,7 +86,7 @@ "INF x. P" == "INF x:UNIV. P"; -lemma ub_ge_sup: "isUb A B y ==> is_Sup A B s ==> s <= y"; +lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y"; by (unfold is_Sup_def, rule isLub_le_isUb); lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s";