--- a/src/HOL/Analysis/Abstract_Limits.thy Fri Apr 05 11:22:00 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Limits.thy Fri Apr 05 15:02:46 2019 +0100
@@ -53,11 +53,11 @@
lemma limitin_topspace: "limitin X f l F \<Longrightarrow> l \<in> topspace X"
by (simp add: limitin_def)
-lemma limitin_const: "limitin X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
+lemma limitin_const_iff [simp]: "limitin X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
by (simp add: limitin_def)
-lemma limitin_real_const: "limitin euclideanreal (\<lambda>a. l) l F"
- by (simp add: limitin_def)
+lemma limitin_const: "limitin euclidean (\<lambda>a. l) l F"
+ by simp
lemma limitin_eventually:
"\<lbrakk>l \<in> topspace X; eventually (\<lambda>x. f x = l) F\<rbrakk> \<Longrightarrow> limitin X f l F"
@@ -91,6 +91,11 @@
qed (auto simp: limitin_def topspace_subtopology)
+lemma limitin_canonical_iff_gen [simp]:
+ assumes "open S"
+ shows "limitin (top_of_set S) f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F \<and> l \<in> S"
+ using assms by (auto simp: limitin_subtopology tendsto_def)
+
lemma limitin_sequentially:
"limitin X S l sequentially \<longleftrightarrow>
l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> (\<exists>N. \<forall>n. N \<le> n \<longrightarrow> S n \<in> U))"