src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 51471 cad22a3cc09c
parent 51365 6b5250100db8
child 51472 adb441e4b9e9
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Mar 21 16:58:14 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:42 2013 +0100
     1.3 @@ -1340,11 +1340,11 @@
     1.4  
     1.5  text {* Some property holds "sufficiently close" to the limit point. *}
     1.6  
     1.7 -lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *)
     1.8 +lemma eventually_at: (* FIXME: this replaces Metric_Spaces.eventually_at *)
     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 Limits.eventually_within *)
    1.13 +lemma eventually_within: (* FIXME: this replaces Topological_Spaces.eventually_within *)
    1.14    "eventually P (at a within S) \<longleftrightarrow>
    1.15          (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
    1.16    by (rule eventually_within_less)
    1.17 @@ -1448,12 +1448,12 @@
    1.18    from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
    1.19    { assume "?lhs"
    1.20      then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
    1.21 -      unfolding Limits.eventually_within Limits.eventually_at_topological
    1.22 +      unfolding Limits.eventually_within eventually_at_topological
    1.23        by auto
    1.24      with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
    1.25        by auto
    1.26      then have "?rhs"
    1.27 -      unfolding Limits.eventually_at_topological by auto
    1.28 +      unfolding eventually_at_topological by auto
    1.29    } moreover
    1.30    { assume "?rhs" hence "?lhs"
    1.31        unfolding Limits.eventually_within