--- 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