src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44668 31d41a0f6b5d
parent 44648 897f32a827f2
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Sep 02 14:27:55 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Sep 02 15:19:59 2011 -0700
     1.3 @@ -914,7 +914,7 @@
     1.4  lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow>
     1.5          (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs")
     1.6  unfolding eventually_within
     1.7 -by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl) 
     1.8 +by auto (metis dense order_le_less_trans)
     1.9  
    1.10  lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
    1.11    unfolding trivial_limit_def