Entry	Value
Package Name	natural-distance-thm
Count	22
Theorems	DIST_ADD2 : !m n p q. dist (m + n) (p + q) <= dist m p + dist n q DIST_ADD2_REV : !m n p q. dist m p <= dist (m + n) (p + q) + dist n q DIST_ADDBOUND : !m n. dist m n <= m + n DIST_CASES : !m n p. dist m n = p <=> m + p = n \/ n + p = m DIST_DIST_SUC : !m n. dist (dist m n) (dist m (n + 1)) = 1 DIST_ELIM_THM : !p x y. p (dist x y) <=> (!d. (x = y + d ==> p d) /\ (y = x + d ==> p d)) DIST_EQ_0 : !m n. dist m n = 0 <=> m = n DIST_LADD : !m n p. dist (m + n) (m + p) = dist n p DIST_LADD_0 : !m n. dist (m + n) m = n DIST_LE_CASES : !m n p. dist m n <= p <=> m <= n + p /\ n <= m + p DIST_LMUL : !m n p. m * dist n p = dist (m * n) (m * p) DIST_LZERO : !n. dist 0 n = n DIST_RADD : !p m n. dist (m + p) (n + p) = dist m n DIST_RADD_0 : !m n. dist m (m + n) = n DIST_REFL : !n. dist n n = 0 DIST_RMUL : !p m n. dist m n * p = dist (m * p) (n * p) DIST_RZERO : !n. dist n 0 = n DIST_SUC : !m n. dist (SUC m) (SUC n) = dist m n DIST_SYM : !m n. dist m n = dist n m DIST_TRIANGLE : !m n p. dist m p <= dist m n + dist n p DIST_TRIANGLES_LE : !m n p q r s. dist m n <= r /\ dist p q <= s ==> dist m p <= dist n q + r + s DIST_TRIANGLE_LE : !m n p q. dist m n + dist n p <= q ==> dist m p <= q

Back to main package page