author hoelzl Tue Mar 26 12:21:00 2013 +0100 (2013-03-26) changeset 51530 609914f0934a parent 51529 2d2f59e6055a child 51531 f415febf4234
rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
```     1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 26 12:21:00 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 26 12:21:00 2013 +0100
1.3 @@ -890,7 +890,7 @@
1.4  lemma Liminf_within:
1.5    fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
1.6    shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
1.7 -  unfolding Liminf_def eventually_within
1.8 +  unfolding Liminf_def eventually_within_less
1.9  proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
1.10    fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
1.11    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
1.12 @@ -908,7 +908,7 @@
1.13  lemma Limsup_within:
1.14    fixes f :: "'a::metric_space => 'b::complete_lattice"
1.15    shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
1.16 -  unfolding Limsup_def eventually_within
1.17 +  unfolding Limsup_def eventually_within_less
1.18  proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
1.19    fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
1.20    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 26 12:21:00 2013 +0100
2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 26 12:21:00 2013 +0100
2.3 @@ -1256,15 +1256,10 @@
2.4
2.5  text {* Some property holds "sufficiently close" to the limit point. *}
2.6
2.7 -lemma eventually_at: (* FIXME: this replaces Metric_Spaces.eventually_at *)
2.8 +lemma eventually_at2:
2.9    "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
2.10  unfolding eventually_at dist_nz by auto
2.11
2.12 -lemma eventually_within: (* FIXME: this replaces Topological_Spaces.eventually_within *)
2.13 -  "eventually P (at a within S) \<longleftrightarrow>
2.14 -        (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
2.15 -  by (rule eventually_within_less)
2.16 -
2.17  lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
2.18    unfolding trivial_limit_def
2.19    by (auto elim: eventually_rev_mp)
2.20 @@ -1301,11 +1296,11 @@
2.21
2.22  lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow>
2.23          (\<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)"
2.24 -  by (auto simp add: tendsto_iff eventually_within)
2.25 +  by (auto simp add: tendsto_iff eventually_within_less)
2.26
2.27  lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
2.28          (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
2.29 -  by (auto simp add: tendsto_iff eventually_at)
2.30 +  by (auto simp add: tendsto_iff eventually_at2)
2.31
2.32  lemma Lim_at_infinity:
2.33    "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)"
2.34 @@ -1601,7 +1596,7 @@
2.35    shows "(g ---> l) (at x within S)"
2.36  proof (rule Lim_transform_eventually)
2.37    show "eventually (\<lambda>x. f x = g x) (at x within S)"
2.38 -    unfolding eventually_within
2.39 +    unfolding eventually_within_less
2.40      using assms(1,2) by auto
2.41    show "(f ---> l) (at x within S)" by fact
2.42  qed
2.43 @@ -1612,7 +1607,7 @@
2.44    shows "(g ---> l) (at x)"
2.45  proof (rule Lim_transform_eventually)
2.46    show "eventually (\<lambda>x. f x = g x) (at x)"
2.47 -    unfolding eventually_at
2.48 +    unfolding eventually_at2
2.49      using assms(1,2) by auto
2.50    show "(f ---> l) (at x)" by fact
2.51  qed
2.52 @@ -3788,7 +3783,7 @@
2.53    { 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"
2.54      fix T::"'b set" assume "open T" and "f a \<in> T"
2.55      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"
2.56 -      unfolding continuous_within tendsto_def eventually_within by auto
2.57 +      unfolding continuous_within tendsto_def eventually_within_less by auto
2.58      have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
2.59        using x(2) `d>0` by simp
2.60      hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
2.61 @@ -4186,8 +4181,7 @@
2.62    hence "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
2.63      using `a \<notin> U` by (fast elim: eventually_mono [rotated])
2.64    thus ?thesis
2.65 -    unfolding Limits.eventually_within Metric_Spaces.eventually_at
2.66 -    by (rule ex_forward, cut_tac `f x \<noteq> a`, auto simp: dist_commute)
2.67 +    using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_within_less)
2.68  qed
2.69
2.70  lemma continuous_at_avoid:
```