summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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