# HG changeset patch # User hoelzl # Date 1364296860 -3600 # Node ID 609914f0934a8409376c0022841b263f0571fab9 # Parent 2d2f59e6055a60876663170bc51080f9384b114b rename eventually_at / _within, to distinguish them from the lemmas in the HOL image diff -r 2d2f59e6055a -r 609914f0934a src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Mar 26 12:21:00 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Mar 26 12:21:00 2013 +0100 @@ -890,7 +890,7 @@ lemma Liminf_within: fixes f :: "'a::metric_space \ 'b::complete_lattice" shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \ ball x e - {x}). f y)" - unfolding Liminf_def eventually_within + unfolding Liminf_def eventually_within_less proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe) fix P d assume "0 < d" "\y. y \ S \ 0 < dist y x \ dist y x < d \ P y" then have "S \ ball x d - {x} \ {x. P x}" @@ -908,7 +908,7 @@ lemma Limsup_within: fixes f :: "'a::metric_space => 'b::complete_lattice" shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \ ball x e - {x}). f y)" - unfolding Limsup_def eventually_within + unfolding Limsup_def eventually_within_less proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe) fix P d assume "0 < d" "\y. y \ S \ 0 < dist y x \ dist y x < d \ P y" then have "S \ ball x d - {x} \ {x. P x}" diff -r 2d2f59e6055a -r 609914f0934a src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Mar 26 12:21:00 2013 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Mar 26 12:21:00 2013 +0100 @@ -1256,15 +1256,10 @@ text {* Some property holds "sufficiently close" to the limit point. *} -lemma eventually_at: (* FIXME: this replaces Metric_Spaces.eventually_at *) +lemma eventually_at2: "eventually P (at a) \ (\d>0. \x. 0 < dist x a \ dist x a < d \ P x)" unfolding eventually_at dist_nz by auto -lemma eventually_within: (* FIXME: this replaces Topological_Spaces.eventually_within *) - "eventually P (at a within S) \ - (\d>0. \x\S. 0 < dist x a \ dist x a < d \ P x)" - by (rule eventually_within_less) - lemma eventually_happens: "eventually P net ==> trivial_limit net \ (\x. P x)" unfolding trivial_limit_def by (auto elim: eventually_rev_mp) @@ -1301,11 +1296,11 @@ lemma Lim_within: "(f ---> l) (at a within S) \ (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" - by (auto simp add: tendsto_iff eventually_within) + by (auto simp add: tendsto_iff eventually_within_less) lemma Lim_at: "(f ---> l) (at a) \ (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" - by (auto simp add: tendsto_iff eventually_at) + by (auto simp add: tendsto_iff eventually_at2) lemma Lim_at_infinity: "(f ---> l) at_infinity \ (\e>0. \b. \x. norm x >= b \ dist (f x) l < e)" @@ -1601,7 +1596,7 @@ shows "(g ---> l) (at x within S)" proof (rule Lim_transform_eventually) show "eventually (\x. f x = g x) (at x within S)" - unfolding eventually_within + unfolding eventually_within_less using assms(1,2) by auto show "(f ---> l) (at x within S)" by fact qed @@ -1612,7 +1607,7 @@ shows "(g ---> l) (at x)" proof (rule Lim_transform_eventually) show "eventually (\x. f x = g x) (at x)" - unfolding eventually_at + unfolding eventually_at2 using assms(1,2) by auto show "(f ---> l) (at x)" by fact qed @@ -3788,7 +3783,7 @@ { fix x::"nat \ 'a" assume x:"\n. x n \ s" "\e>0. eventually (\n. dist (x n) a < e) sequentially" fix T::"'b set" assume "open T" and "f a \ T" with `?lhs` obtain d where "d>0" and d:"\x\s. 0 < dist x a \ dist x a < d \ f x \ T" - unfolding continuous_within tendsto_def eventually_within by auto + unfolding continuous_within tendsto_def eventually_within_less by auto have "eventually (\n. dist (x n) a < d) sequentially" using x(2) `d>0` by simp hence "eventually (\n. (f \ x) n \ T) sequentially" @@ -4186,8 +4181,7 @@ hence "eventually (\y. f y \ a) (at x within s)" using `a \ U` by (fast elim: eventually_mono [rotated]) thus ?thesis - unfolding Limits.eventually_within Metric_Spaces.eventually_at - by (rule ex_forward, cut_tac `f x \ a`, auto simp: dist_commute) + using `f x \ a` by (auto simp: dist_commute zero_less_dist_iff eventually_within_less) qed lemma continuous_at_avoid: