| changeset 31565 | da5a5589418e |
| parent 31564 | d2abf6f6f619 |
| child 31567 | 0fb78b3a9145 |
--- a/src/HOL/RealVector.thy Thu Jun 11 10:37:02 2009 -0700 +++ b/src/HOL/RealVector.thy Thu Jun 11 11:51:12 2009 -0700 @@ -530,6 +530,9 @@ lemma dist_triangle: "dist x z \<le> dist x y + dist y z" using dist_triangle2 [of x z y] by (simp add: dist_commute) +lemma dist_triangle3: "dist x y \<le> dist a x + dist a y" +using dist_triangle2 [of x y a] by (simp add: dist_commute) + subclass topological_space proof have "\<exists>e::real. 0 < e"