# HG changeset patch
# User huffman
# Date 1316541761 25200
# Node ID 5a4d62f9e88de2c37cc27fd8cdaf55b441ee2dd7
# Parent  9583f2b56f85e50860a1f5c4877c701a9670dfad
Extended_Real_Limits: generalize some lemmas

diff -r 9583f2b56f85 -r 5a4d62f9e88d src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Sep 20 10:52:08 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Sep 20 11:02:41 2011 -0700
@@ -750,21 +750,20 @@
   using Limsup_within[of x UNIV f] by simp
 
 lemma Lim_within_constant:
-  fixes f :: "'a::metric_space => 'b::topological_space"
   assumes "ALL y:S. f y = C"
   shows "(f ---> C) (at x within S)"
-unfolding tendsto_def eventually_within
-by (metis assms(1) linorder_le_less_linear n_not_Suc_n real_of_nat_le_zero_cancel_iff)
+  unfolding tendsto_def Limits.eventually_within eventually_at_topological
+  using assms by simp (metis open_UNIV UNIV_I)
 
 lemma Liminf_within_constant:
-  fixes f :: "'a::metric_space => ereal"
+  fixes f :: "'a::topological_space \<Rightarrow> ereal"
   assumes "ALL y:S. f y = C"
   assumes "~trivial_limit (at x within S)"
   shows "Liminf (at x within S) f = C"
 by (metis Lim_within_constant assms lim_imp_Liminf)
 
 lemma Limsup_within_constant:
-  fixes f :: "'a::metric_space => ereal"
+  fixes f :: "'a::topological_space \<Rightarrow> ereal"
   assumes "ALL y:S. f y = C"
   assumes "~trivial_limit (at x within S)"
   shows "Limsup (at x within S) f = C"