src/probability/real_topologyScript.sml

1484 val between = new_definition ("between",
1485  ``between x (a,b) <=> (dist(a,b) = dist(a,x) + dist(x,b))``);
1488  ``!a b. between a (a,b) /\ between b (a,b) /\ between a (a,a)``,
1489   REWRITE_TAC[between, dist] THEN REAL_ARITH_TAC);
1492  ``!a x. between x (a,a) <=> (x = a)``,
1493   REWRITE_TAC[between, dist] THEN REAL_ARITH_TAC);
1496  ``!a b x. between x (a,b) <=> between x (b,a)``,
1497   REWRITE_TAC[between, dist] THEN REAL_ARITH_TAC);
1500  ``!a b c. between a (b,c) /\ between b (a,c) ==> (a = b)``,
1501   REWRITE_TAC[between, dist] THEN REAL_ARITH_TAC);
1504  ``!a b c d. between a (b,c) /\ between d (a,c) ==> between d (b,c)``,
1505   REWRITE_TAC[between, dist] THEN REAL_ARITH_TAC);
1508  ``!a b c d. between a (b,c) /\ between d (a,b) ==> between a (c,d)``,
1509   REWRITE_TAC[between, dist] THEN REAL_ARITH_TAC);
1513      between x (a,b) <=> (abs(x - a) * (b - x) = abs(b - x) * (x - a))``,
1514   REPEAT GEN_TAC THEN REWRITE_TAC[between, DIST_TRIANGLE_EQ] THEN
1518  ``!a b x:real. between x (a,b) ==> collinear {a;x;b}``,
1533         between a (b,c) \/ between b (c,a) \/ between c (a,b)``,
1537     STRIP_TAC THEN ASM_REWRITE_TAC[between, dist] THEN
1546            ==> between x (a,b)``,
1547   SIMP_TAC std_ss [COLLINEAR_BETWEEN_CASES, between, dist] THEN REAL_ARITH_TAC);
1557   REWRITE_TAC[between, dist, ABS_N] THEN
1561 (* Midpoint between two points.                                              *)
1599  ``!a b. between (midpoint(a,b)) (a,b) /\ between (midpoint(a,b)) (b,a)``,
1600   REWRITE_TAC[between, midpoint] THEN ONCE_REWRITE_TAC [REAL_MUL_SYM] THEN
3340  ``!x a b:real. between x (a,b) <=> x IN segment[a,b]``,
3341   REPEAT GEN_TAC THEN REWRITE_TAC[between] THEN
5931 (* Interrelations between restricted and unrestricted limits.                *)
14139 (* Separation between points and sets.                                       *)
15202               EXTENSION, GSYM BETWEEN_IN_SEGMENT, between, IN_INTERVAL] THEN
16781 (* Homeomorphisms between open intervals in real and then in real.       *)
19600 (* More general infimum of distance between two sets.                        *)
20465 (* Hausdorff distance between sets.                                          *)