--- a/src/HOL/Analysis/Connected.thy Mon Oct 30 21:52:31 2017 +0100
+++ b/src/HOL/Analysis/Connected.thy Mon Oct 30 19:29:06 2017 +0000
@@ -168,7 +168,7 @@
apply (rule subsetD [OF closure_subset], simp)
apply (simp add: closure_def, clarify)
apply (rule closure_ball_lemma)
- apply (simp add: zero_less_dist_iff)
+ apply simp
done
(* In a trivial vector space, this fails for e = 0. *)
@@ -1969,7 +1969,7 @@
then have "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
using \<open>a \<notin> U\<close> by (fast elim: eventually_mono)
then show ?thesis
- using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute zero_less_dist_iff eventually_at)
+ using \<open>f x \<noteq> a\<close> by (auto simp: dist_commute eventually_at)
qed
lemma continuous_at_avoid:
@@ -3022,9 +3022,7 @@
lemma translation_UNIV:
fixes a :: "'a::ab_group_add"
shows "range (\<lambda>x. a + x) = UNIV"
- apply (auto simp: image_iff)
- apply (rule_tac x="x - a" in exI, auto)
- done
+ by (fact surj_plus)
lemma translation_diff:
fixes a :: "'a::ab_group_add"
--- a/src/HOL/Nat.thy Mon Oct 30 21:52:31 2017 +0100
+++ b/src/HOL/Nat.thy Mon Oct 30 19:29:06 2017 +0000
@@ -190,6 +190,15 @@
end
+context ab_group_add
+begin
+
+lemma surj_plus [simp]:
+ "surj (plus a)"
+ by (auto intro: range_eqI [of b "plus a" "b - a" for b] simp add: algebra_simps)
+
+end
+
context semidom_divide
begin