src/HOL/Real_Vector_Spaces.thy
changeset 62397 5ae24f33d343
parent 62379 340738057c8c
child 62533 bc25f3916a99
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Feb 23 15:49:17 2016 +0000
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Feb 24 15:51:01 2016 +0000
     1.3 @@ -1308,6 +1308,11 @@
     1.4  
     1.5  declare norm_conv_dist [symmetric, simp]
     1.6  
     1.7 +lemma dist_0_norm [simp]:
     1.8 +  fixes x :: "'a::real_normed_vector"
     1.9 +  shows "dist 0 x = norm x"
    1.10 +unfolding dist_norm by simp
    1.11 +
    1.12  lemma dist_diff [simp]: "dist a (a - b) = norm b"  "dist (a - b) a = norm b"
    1.13    by (simp_all add: dist_norm)
    1.14