src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 51530 609914f0934a
parent 51518 6a56b7088a6a
child 51641 cd05e9fcc63d
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 26 12:21:00 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 26 12:21:00 2013 +0100
     1.3 @@ -1256,15 +1256,10 @@
     1.4  
     1.5  text {* Some property holds "sufficiently close" to the limit point. *}
     1.6  
     1.7 -lemma eventually_at: (* FIXME: this replaces Metric_Spaces.eventually_at *)
     1.8 +lemma eventually_at2:
     1.9    "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
    1.10  unfolding eventually_at dist_nz by auto
    1.11  
    1.12 -lemma eventually_within: (* FIXME: this replaces Topological_Spaces.eventually_within *)
    1.13 -  "eventually P (at a within S) \<longleftrightarrow>
    1.14 -        (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
    1.15 -  by (rule eventually_within_less)
    1.16 -
    1.17  lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
    1.18    unfolding trivial_limit_def
    1.19    by (auto elim: eventually_rev_mp)
    1.20 @@ -1301,11 +1296,11 @@
    1.21  
    1.22  lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow>
    1.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)"
    1.24 -  by (auto simp add: tendsto_iff eventually_within)
    1.25 +  by (auto simp add: tendsto_iff eventually_within_less)
    1.26  
    1.27  lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
    1.28          (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
    1.29 -  by (auto simp add: tendsto_iff eventually_at)
    1.30 +  by (auto simp add: tendsto_iff eventually_at2)
    1.31  
    1.32  lemma Lim_at_infinity:
    1.33    "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)"
    1.34 @@ -1601,7 +1596,7 @@
    1.35    shows "(g ---> l) (at x within S)"
    1.36  proof (rule Lim_transform_eventually)
    1.37    show "eventually (\<lambda>x. f x = g x) (at x within S)"
    1.38 -    unfolding eventually_within
    1.39 +    unfolding eventually_within_less
    1.40      using assms(1,2) by auto
    1.41    show "(f ---> l) (at x within S)" by fact
    1.42  qed
    1.43 @@ -1612,7 +1607,7 @@
    1.44    shows "(g ---> l) (at x)"
    1.45  proof (rule Lim_transform_eventually)
    1.46    show "eventually (\<lambda>x. f x = g x) (at x)"
    1.47 -    unfolding eventually_at
    1.48 +    unfolding eventually_at2
    1.49      using assms(1,2) by auto
    1.50    show "(f ---> l) (at x)" by fact
    1.51  qed
    1.52 @@ -3788,7 +3783,7 @@
    1.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"
    1.54      fix T::"'b set" assume "open T" and "f a \<in> T"
    1.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"
    1.56 -      unfolding continuous_within tendsto_def eventually_within by auto
    1.57 +      unfolding continuous_within tendsto_def eventually_within_less by auto
    1.58      have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
    1.59        using x(2) `d>0` by simp
    1.60      hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
    1.61 @@ -4186,8 +4181,7 @@
    1.62    hence "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
    1.63      using `a \<notin> U` by (fast elim: eventually_mono [rotated])
    1.64    thus ?thesis
    1.65 -    unfolding Limits.eventually_within Metric_Spaces.eventually_at
    1.66 -    by (rule ex_forward, cut_tac `f x \<noteq> a`, auto simp: dist_commute)
    1.67 +    using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_within_less)
    1.68  qed
    1.69  
    1.70  lemma continuous_at_avoid: