--- a/src/HOL/Limits.thy Fri Nov 01 19:40:55 2019 +0100
+++ b/src/HOL/Limits.thy Sat Nov 02 14:31:34 2019 +0000
@@ -703,7 +703,7 @@
subsubsection \<open>Linear operators and multiplication\<close>
-lemma linear_times: "linear (\<lambda>x. c * x)"
+lemma linear_times [simp]: "linear (\<lambda>x. c * x)"
for c :: "'a::real_algebra"
by (auto simp: linearI distrib_left)
@@ -2472,6 +2472,12 @@
for f :: "'a :: real_normed_vector \<Rightarrow> _"
using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
+lemma tendsto_offset_zero_iff:
+ fixes f :: "'a :: real_normed_vector \<Rightarrow> _"
+ assumes "a \<in> S" "open S"
+ shows "(f \<longlongrightarrow> L) (at a within S) \<longleftrightarrow> ((\<lambda>h. f (a + h)) \<longlongrightarrow> L) (at 0)"
+ by (metis LIM_offset_zero_iff assms tendsto_within_open)
+
lemma LIM_zero: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. f x - l) \<longlongrightarrow> 0) F"
for f :: "'a \<Rightarrow> 'b::real_normed_vector"
unfolding tendsto_iff dist_norm by simp