src/HOL/Groups.thy
changeset 60762 bf0c76ccee8d
parent 60758 d8d85a8172b5
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Groups.thy	Mon Jul 20 11:40:43 2015 +0200
     1.2 +++ b/src/HOL/Groups.thy	Mon Jul 20 23:12:50 2015 +0100
     1.3 @@ -1372,6 +1372,15 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma dense_eq0_I:
     1.8 +  fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
     1.9 +  shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
    1.10 +  apply (cases "abs x=0", simp)
    1.11 +  apply (simp only: zero_less_abs_iff [symmetric])
    1.12 +  apply (drule dense)
    1.13 +  apply (auto simp add: not_less [symmetric])
    1.14 +  done
    1.15 +
    1.16  hide_fact (open) ab_diff_conv_add_uminus add_0 mult_1 ab_left_minus
    1.17  
    1.18  lemmas add_0 = add_0_left -- \<open>FIXME duplicate\<close>