src/HOL/Analysis/Norm_Arith.thy
changeset 68607 67bb59e49834
parent 67962 0acdcd8f4ba1
child 69517 dc20f278e8f3
     1.1 --- a/src/HOL/Analysis/Norm_Arith.thy	Mon Jul 09 21:55:40 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Norm_Arith.thy	Tue Jul 10 09:38:35 2018 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4  
     1.5  text \<open>Hence more metric properties.\<close>
     1.6  
     1.7 -lemma%important dist_triangle_add:
     1.8 +proposition dist_triangle_add:
     1.9    fixes x y x' y' :: "'a::real_normed_vector"
    1.10    shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
    1.11    by norm