--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy Thu Aug 15 16:11:56 2019 +0100
@@ -495,9 +495,9 @@
done
lemma Lim_transform_within_set_eq:
- fixes a l :: "'a::real_normed_vector"
- shows "eventually (\<lambda>x. x \<in> s \<longleftrightarrow> x \<in> t) (at a)
- \<Longrightarrow> ((f \<longlongrightarrow> l) (at a within s) \<longleftrightarrow> (f \<longlongrightarrow> l) (at a within t))"
+ fixes a :: "'a::metric_space" and l :: "'b::metric_space"
+ shows "eventually (\<lambda>x. x \<in> S \<longleftrightarrow> x \<in> T) (at a)
+ \<Longrightarrow> ((f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l) (at a within T))"
by (force intro: Lim_transform_within_set elim: eventually_mono)
lemma Lim_null: