equal
deleted
inserted
replaced
72 -------------------------------------------------------*) |
72 -------------------------------------------------------*) |
73 |
73 |
74 lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)" |
74 lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)" |
75 apply (frule isLub_isUb) |
75 apply (frule isLub_isUb) |
76 apply (frule_tac x = y in isLub_isUb) |
76 apply (frule_tac x = y in isLub_isUb) |
77 apply (blast intro!: real_le_anti_sym dest!: isLub_le_isUb) |
77 apply (blast intro!: order_antisym dest!: isLub_le_isUb) |
78 done |
78 done |
79 |
79 |
80 lemma real_order_restrict: "[| (x::real) <=* S'; S <= S' |] ==> x <=* S" |
80 lemma real_order_restrict: "[| (x::real) <=* S'; S <= S' |] ==> x <=* S" |
81 by (unfold setle_def setge_def, blast) |
81 by (unfold setle_def setge_def, blast) |
82 |
82 |