added lemma
authorhaftmann
Mon Oct 30 19:29:06 2017 +0000 (19 months ago)
changeset 66953826a5fd4d36c
parent 66952 80985b62029d
child 66954 0230af0f3c59
added lemma
src/HOL/Analysis/Connected.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Analysis/Connected.thy	Mon Oct 30 21:52:31 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Connected.thy	Mon Oct 30 19:29:06 2017 +0000
     1.3 @@ -168,7 +168,7 @@
     1.4    apply (rule subsetD [OF closure_subset], simp)
     1.5    apply (simp add: closure_def, clarify)
     1.6    apply (rule closure_ball_lemma)
     1.7 -  apply (simp add: zero_less_dist_iff)
     1.8 +  apply simp
     1.9    done
    1.10  
    1.11  (* In a trivial vector space, this fails for e = 0. *)
    1.12 @@ -1969,7 +1969,7 @@
    1.13    then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
    1.14      using \<open>a \<notin> U\<close> by (fast elim: eventually_mono)
    1.15    then show ?thesis
    1.16 -    using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute zero_less_dist_iff eventually_at)
    1.17 +    using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute eventually_at)
    1.18  qed
    1.19  
    1.20  lemma continuous_at_avoid:
    1.21 @@ -3022,9 +3022,7 @@
    1.22  lemma translation_UNIV:
    1.23    fixes a :: "'a::ab_group_add"
    1.24    shows "range (\<lambda>x. a + x) = UNIV"
    1.25 -  apply (auto simp: image_iff)
    1.26 -  apply (rule_tac x="x - a" in exI, auto)
    1.27 -  done
    1.28 +  by (fact surj_plus)
    1.29  
    1.30  lemma translation_diff:
    1.31    fixes a :: "'a::ab_group_add"
     2.1 --- a/src/HOL/Nat.thy	Mon Oct 30 21:52:31 2017 +0100
     2.2 +++ b/src/HOL/Nat.thy	Mon Oct 30 19:29:06 2017 +0000
     2.3 @@ -190,6 +190,15 @@
     2.4  
     2.5  end
     2.6  
     2.7 +context ab_group_add
     2.8 +begin
     2.9 +
    2.10 +lemma surj_plus [simp]:
    2.11 +  "surj (plus a)"
    2.12 +  by (auto intro: range_eqI [of b "plus a" "b - a" for b] simp add: algebra_simps)
    2.13 +
    2.14 +end
    2.15 +
    2.16  context semidom_divide
    2.17  begin
    2.18