--- a/src/HOL/Analysis/Complex_Transcendental.thy Wed Jul 17 14:02:50 2019 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Wed Jul 17 16:32:06 2019 +0100
@@ -2631,7 +2631,7 @@
have "(\<lambda>n. ln(1 + 1/n) / ln n) \<longlonglongrightarrow> 0"
proof (rule Lim_transform_bound)
show "(inverse o real) \<longlonglongrightarrow> 0"
- by (metis comp_def lim_inverse_n tendsto_explicit)
+ by (metis comp_def lim_inverse_n lim_explicit)
show "\<forall>\<^sub>F n in sequentially. norm (ln (1 + 1 / n) / ln n) \<le> norm ((inverse \<circ> real) n)"
proof
fix n::nat
--- a/src/HOL/Library/Extended_Real.thy Wed Jul 17 14:02:50 2019 +0100
+++ b/src/HOL/Library/Extended_Real.thy Wed Jul 17 16:32:06 2019 +0100
@@ -3172,7 +3172,7 @@
and "f0 \<in> S"
obtains N where "\<forall>n\<ge>N. f n \<in> S"
using assms using tendsto_def
- using tendsto_explicit[of f f0] assms by auto
+ using lim_explicit[of f f0] assms by auto
lemma ereal_LimI_finite_iff:
fixes x :: ereal
--- a/src/HOL/Topological_Spaces.thy Wed Jul 17 14:02:50 2019 +0100
+++ b/src/HOL/Topological_Spaces.thy Wed Jul 17 16:32:06 2019 +0100
@@ -1145,7 +1145,7 @@
lemma lim_def: "lim X = (THE L. X \<longlonglongrightarrow> L)"
unfolding Lim_def ..
-lemma tendsto_explicit:
+lemma lim_explicit:
"f \<longlonglongrightarrow> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
unfolding tendsto_def eventually_sequentially by auto