rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
authorhoelzl
Tue Mar 26 12:21:00 2013 +0100 (2013-03-26)
changeset 51530609914f0934a
parent 51529 2d2f59e6055a
child 51531 f415febf4234
rename eventually_at / _within, to distinguish them from the lemmas in the HOL image
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     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: