Lines Matching defs:convex
45 (* convex *)
48 val convex = new_definition ("convex",
49 ``convex (s:real->bool) <=>
54 !s. convex s <=> !x y u. x IN s /\ y IN s /\ &0 <= u /\ u <= &1
57 GEN_TAC >> REWRITE_TAC [convex] THEN
65 convex s /\ a IN s /\ b IN s /\ &0 <= u /\ u <= &1
76 !s x:real. convex s /\ x IN s ==> (x limit_point_of s <=> ~(s = {x}))
109 convex s /\ x IN s ==> (trivial_limit(at x within s) <=> (s = {x}))``,
117 ``!s:real->bool. convex s ==> connected s``,
143 FINITE k /\ convex s /\ (sum k u = &1) /\
147 GEN_TAC THEN ASM_CASES_TAC ``convex(s:real->bool)`` THEN
186 UNDISCH_TAC ``convex s`` THEN DISCH_TAC THEN
187 FIRST_X_ASSUM(MP_TAC o REWRITE_RULE [convex]) THEN
205 convex s <=>
212 DISCH_TAC THEN REWRITE_TAC[convex] THEN
225 ``!s:real->bool. is_interval s ==> convex s``,
226 REWRITE_TAC[is_interval, convex] THEN
263 ``!a b:real. convex(interval [a,b]) /\ convex(interval (a,b))``,
268 (* On real, is_interval, convex and connected are all equivalent. *)
272 ``!s:real->bool. is_interval s <=> convex s``,
329 ``!x:real e. convex(ball(x,e))``,
330 SIMP_TAC std_ss [convex, IN_BALL] THEN REPEAT STRIP_TAC THEN
783 x IN s /\ convex s /\ (f has_derivative f') (at x within s) /\
916 x IN s /\ convex s /\ (f has_derivative f') (at x within s) /\
928 ``!x:real e. convex(cball(x,e))``,
929 REWRITE_TAC[convex, IN_CBALL, dist] THEN MAP_EVERY X_GEN_TAC
1177 convex s /\
1260 convex s /\
1306 convex s /\
1475 convex s /\
1496 convex s /\