author huffman Tue, 20 Sep 2011 11:02:41 -0700 changeset 45032 5a4d62f9e88d parent 45031 9583f2b56f85 child 45033 34e5fc15ea02
Extended_Real_Limits: generalize some lemmas
```--- 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"```