src/HOL/Real_Vector_Spaces.thy
changeset 62087 44841d07ef1d
parent 62049 b0f941e207cf
child 62101 26c0a70f78a3
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Jan 06 16:17:50 2016 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Jan 07 17:40:55 2016 +0000
     1.3 @@ -1056,6 +1056,8 @@
     1.4    shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
     1.5  by (simp add: zero_less_dist_iff)
     1.6  
     1.7 +declare dist_nz [symmetric, simp]
     1.8 +
     1.9  lemma dist_triangle_le:
    1.10    shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
    1.11  by (rule order_trans [OF dist_triangle2])
    1.12 @@ -1673,7 +1675,7 @@
    1.13  lemma eventually_at:
    1.14    fixes a :: "'a :: metric_space"
    1.15    shows "eventually P (at a within S) \<longleftrightarrow> (\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<and> dist x a < d \<longrightarrow> P x)"
    1.16 -  unfolding eventually_at_filter eventually_nhds_metric by (auto simp: dist_nz)
    1.17 +  unfolding eventually_at_filter eventually_nhds_metric by auto
    1.18  
    1.19  lemma eventually_at_le:
    1.20    fixes a :: "'a::metric_space"