author hoelzl Tue, 26 Mar 2013 12:21:00 +0100 changeset 51530 609914f0934a parent 51529 2d2f59e6055a child 51531 f415febf4234
rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
```--- 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 \<Rightarrow> 'b::complete_lattice"
shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> 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" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
then have "S \<inter> ball x d - {x} \<subseteq> {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 \<inter> 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" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"```
```--- 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) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> 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) \<longleftrightarrow>
-        (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
-  by (rule eventually_within_less)
-
lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>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) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x \<in> S. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> 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) \<longleftrightarrow>
(\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> 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 \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)"
@@ -1601,7 +1596,7 @@
shows "(g ---> l) (at x within S)"
proof (rule Lim_transform_eventually)
show "eventually (\<lambda>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 (\<lambda>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 \<Rightarrow> 'a" assume x:"\<forall>n. x n \<in> s" "\<forall>e>0. eventually (\<lambda>n. dist (x n) a < e) sequentially"
fix T::"'b set" assume "open T" and "f a \<in> T"
with `?lhs` obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
-      unfolding continuous_within tendsto_def eventually_within by auto
+      unfolding continuous_within tendsto_def eventually_within_less by auto
have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
using x(2) `d>0` by simp
hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
@@ -4186,8 +4181,7 @@
hence "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
using `a \<notin> 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 \<noteq> a`, auto simp: dist_commute)
+    using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_within_less)
qed

lemma continuous_at_avoid:```