src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 51641 cd05e9fcc63d parent 51530 609914f0934a child 51773 9328c6681f3c
1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Apr 08 21:01:59 2013 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Apr 09 14:04:41 2013 +0200
1.3 @@ -39,9 +39,6 @@
1.4    shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
1.5    by (fact tendsto_within_open)
1.7 -lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
1.8 -  by (fact tendsto_within_subset)
1.9 -
1.10  lemma continuous_on_union:
1.11    "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
1.12    by (fact continuous_on_closed_Un)
1.13 @@ -1205,7 +1202,7 @@
1.14  definition
1.15    indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
1.16      (infixr "indirection" 70) where
1.17 -  "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
1.18 +  "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
1.20  text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
1.22 @@ -1215,7 +1212,7 @@
1.23    assume "trivial_limit (at a within S)"
1.24    thus "\<not> a islimpt S"
1.25      unfolding trivial_limit_def
1.26 -    unfolding eventually_within eventually_at_topological
1.27 +    unfolding eventually_at_topological
1.28      unfolding islimpt_def
1.29      apply (clarsimp simp add: set_eq_iff)
1.30      apply (rename_tac T, rule_tac x=T in exI)
1.31 @@ -1225,7 +1222,7 @@
1.32    assume "\<not> a islimpt S"
1.33    thus "trivial_limit (at a within S)"
1.34      unfolding trivial_limit_def
1.35 -    unfolding eventually_within eventually_at_topological
1.36 +    unfolding eventually_at_topological
1.37      unfolding islimpt_def
1.38      apply clarsimp
1.39      apply (rule_tac x=T in exI)
1.40 @@ -1292,11 +1289,11 @@
1.42  lemma Lim_within_le: "(f ---> l)(at a within S) \<longleftrightarrow>
1.43             (\<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.44 -  by (auto simp add: tendsto_iff eventually_within_le)
1.45 +  by (auto simp add: tendsto_iff eventually_at_le dist_nz)
1.47  lemma Lim_within: "(f ---> l) (at a within S) \<longleftrightarrow>
1.48          (\<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.49 -  by (auto simp add: tendsto_iff eventually_within_less)
1.50 +  by (auto simp add: tendsto_iff eventually_at dist_nz)
1.52  lemma Lim_at: "(f ---> l) (at a) \<longleftrightarrow>
1.53          (\<forall>e >0. \<exists>d>0. \<forall>x. 0 < dist x a  \<and> dist x a  < d  \<longrightarrow> dist (f x) l < e)"
1.54 @@ -1311,12 +1308,12 @@
1.56  text{* The expected monotonicity property. *}
1.58 -lemma Lim_within_empty: "(f ---> l) (net within {})"
1.59 -  unfolding tendsto_def Limits.eventually_within by simp
1.60 -
1.61 -lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
1.62 -  shows "(f ---> l) (net within (S \<union> T))"
1.63 -  using assms unfolding tendsto_def Limits.eventually_within
1.64 +lemma Lim_within_empty: "(f ---> l) (at x within {})"
1.65 +  unfolding tendsto_def eventually_at_filter by simp
1.66 +
1.67 +lemma Lim_Un: assumes "(f ---> l) (at x within S)" "(f ---> l) (at x within T)"
1.68 +  shows "(f ---> l) (at x within (S \<union> T))"
1.69 +  using assms unfolding tendsto_def eventually_at_filter
1.70    apply clarify
1.71    apply (drule spec, drule (1) mp, drule (1) mp)
1.72    apply (drule spec, drule (1) mp, drule (1) mp)
1.73 @@ -1324,17 +1321,16 @@
1.74    done
1.76  lemma Lim_Un_univ:
1.77 - "(f ---> l) (net within S) \<Longrightarrow> (f ---> l) (net within T) \<Longrightarrow>  S \<union> T = UNIV
1.78 -        ==> (f ---> l) net"
1.79 -  by (metis Lim_Un within_UNIV)
1.80 + "(f ---> l) (at x within S) \<Longrightarrow> (f ---> l) (at x within T) \<Longrightarrow>  S \<union> T = UNIV
1.81 +        ==> (f ---> l) (at x)"
1.82 +  by (metis Lim_Un)
1.84  text{* Interrelations between restricted and unrestricted limits. *}
1.86 -lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
1.87 -  (* FIXME: rename *)
1.88 -  unfolding tendsto_def Limits.eventually_within
1.89 -  apply (clarify, drule spec, drule (1) mp, drule (1) mp)
1.90 -  by (auto elim!: eventually_elim1)
1.91 +
1.92 +lemma Lim_at_within: (* FIXME: rename *)
1.93 +  "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
1.94 +  by (metis order_refl filterlim_mono subset_UNIV at_le)
1.96  lemma eventually_within_interior:
1.97    assumes "x \<in> interior S"
1.98 @@ -1343,7 +1339,7 @@
1.99    from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
1.100    { assume "?lhs"
1.101      then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
1.102 -      unfolding Limits.eventually_within eventually_at_topological
1.103 +      unfolding eventually_at_topological
1.104        by auto
1.105      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.106        by auto
1.107 @@ -1351,15 +1347,14 @@
1.108        unfolding eventually_at_topological by auto
1.109    } moreover
1.110    { assume "?rhs" hence "?lhs"
1.111 -      unfolding Limits.eventually_within
1.112 -      by (auto elim: eventually_elim1)
1.113 +      by (auto elim: eventually_elim1 simp: eventually_at_filter)
1.114    } ultimately
1.115    show "?thesis" ..
1.116  qed
1.118  lemma at_within_interior:
1.119    "x \<in> interior S \<Longrightarrow> at x within S = at x"
1.120 -  by (simp add: filter_eq_iff eventually_within_interior)
1.121 +  unfolding filter_eq_iff by (intro allI eventually_within_interior)
1.123  lemma Lim_within_LIMSEQ:
1.124    fixes a :: "'a::metric_space"
1.125 @@ -1386,17 +1381,14 @@
1.126          by (auto intro: cInf_lower)
1.127        with a have "a < f y" by (blast intro: less_le_trans) }
1.128      then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
1.129 -      by (auto simp: Topological_Spaces.eventually_within intro: exI[of _ 1] zero_less_one)
1.130 +      by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
1.131    next
1.132      fix a assume "Inf (f ` ({x<..} \<inter> I)) < a"
1.133      from cInf_lessD[OF _ this] e obtain y where y: "x < y" "y \<in> I" "f y < a" by auto
1.134 -    show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
1.135 -      unfolding within_within_eq[symmetric]
1.136 -        Topological_Spaces.eventually_within[of _ _ I] eventually_at_right
1.137 -    proof (safe intro!: exI[of _ y] y)
1.138 -      fix z assume "x < z" "z \<in> I" "z < y"
1.139 -      with mono[OF `z\<in>I` `y\<in>I`] `f y < a` show "f z < a" by (auto simp: less_imp_le)
1.140 -    qed
1.141 +    then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
1.142 +      unfolding eventually_at_right by (metis less_imp_le le_less_trans mono)
1.143 +    then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
1.144 +      unfolding eventually_at_filter by eventually_elim simp
1.145    qed
1.146  qed
1.148 @@ -1540,7 +1532,7 @@
1.149  text{* These are special for limits out of the same vector space. *}
1.151  lemma Lim_within_id: "(id ---> a) (at a within s)"
1.152 -  unfolding id_def by (rule tendsto_ident_at_within)
1.153 +  unfolding id_def by (rule tendsto_ident_at)
1.155  lemma Lim_at_id: "(id ---> a) (at a)"
1.156    unfolding id_def by (rule tendsto_ident_at)
1.157 @@ -1567,13 +1559,13 @@
1.159  lemma lim_within_interior:
1.160    "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
1.161 -  by (simp add: at_within_interior)
1.162 +  by (metis at_within_interior)
1.164  lemma netlimit_within_interior:
1.165    fixes x :: "'a::{t2_space,perfect_space}"
1.166    assumes "x \<in> interior S"
1.167    shows "netlimit (at x within S) = x"
1.168 -using assms by (simp add: at_within_interior netlimit_at)
1.169 +using assms by (metis at_within_interior netlimit_at)
1.171  text{* Transformation of limit. *}
1.173 @@ -1596,8 +1588,7 @@
1.174    shows "(g ---> l) (at x within S)"
1.175  proof (rule Lim_transform_eventually)
1.176    show "eventually (\<lambda>x. f x = g x) (at x within S)"
1.177 -    unfolding eventually_within_less
1.178 -    using assms(1,2) by auto
1.179 +    using assms(1,2) by (auto simp: dist_nz eventually_at)
1.180    show "(f ---> l) (at x within S)" by fact
1.181  qed
1.183 @@ -1622,7 +1613,7 @@
1.184  proof (rule Lim_transform_eventually)
1.185    show "(f ---> l) (at a within S)" by fact
1.186    show "eventually (\<lambda>x. f x = g x) (at a within S)"
1.187 -    unfolding Limits.eventually_within eventually_at_topological
1.188 +    unfolding eventually_at_topological
1.189      by (rule exI [where x="- {b}"], simp add: open_Compl assms)
1.190  qed
1.192 @@ -1655,7 +1646,7 @@
1.193    assumes "a = b" "x = y" "S = T"
1.194    assumes "\<And>x. x \<noteq> b \<Longrightarrow> x \<in> T \<Longrightarrow> f x = g x"
1.195    shows "(f ---> x) (at a within S) \<longleftrightarrow> (g ---> y) (at b within T)"
1.196 -  unfolding tendsto_def Limits.eventually_within eventually_at_topological
1.197 +  unfolding tendsto_def eventually_at_topological
1.198    using assms by simp
1.200  lemma Lim_cong_at(*[cong add]*):
1.201 @@ -3759,7 +3750,7 @@
1.202  lemma continuous_within_subset:
1.203   "continuous (at x within s) f \<Longrightarrow> t \<subseteq> s
1.204               ==> continuous (at x within t) f"
1.205 -  unfolding continuous_within by(metis Lim_within_subset)
1.206 +  unfolding continuous_within by(metis tendsto_within_subset)
1.208  lemma continuous_on_interior:
1.209    shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
1.210 @@ -3768,7 +3759,7 @@
1.212  lemma continuous_on_eq:
1.213    "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
1.214 -  unfolding continuous_on_def tendsto_def Limits.eventually_within
1.215 +  unfolding continuous_on_def tendsto_def eventually_at_topological
1.216    by simp
1.218  text {* Characterization of various kinds of continuity in terms of sequences. *}
1.219 @@ -3783,7 +3774,7 @@
1.220    { 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.221      fix T::"'b set" assume "open T" and "f a \<in> T"
1.222      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.223 -      unfolding continuous_within tendsto_def eventually_within_less by auto
1.224 +      unfolding continuous_within tendsto_def eventually_at by (auto simp: dist_nz)
1.225      have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
1.226        using x(2) `d>0` by simp
1.227      hence "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
1.228 @@ -4015,7 +4006,7 @@
1.230  lemma continuous_at_open:
1.231    shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))"
1.232 -unfolding continuous_within_topological [of x UNIV f, unfolded within_UNIV]
1.233 +unfolding continuous_within_topological [of x UNIV f]
1.234  unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto
1.236  lemma continuous_imp_tendsto:
1.237 @@ -4181,7 +4172,7 @@
1.238    hence "eventually (\<lambda>y. f y \<noteq> a) (at x within s)"
1.239      using `a \<notin> U` by (fast elim: eventually_mono [rotated])
1.240    thus ?thesis
1.241 -    using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_within_less)
1.242 +    using `f x \<noteq> a` by (auto simp: dist_commute zero_less_dist_iff eventually_at)
1.243  qed
1.245  lemma continuous_at_avoid:
1.246 @@ -4514,7 +4505,7 @@
1.247  proof (rule continuous_attains_sup [OF assms])
1.248    { fix x assume "x\<in>s"
1.249      have "(dist a ---> dist a x) (at x within s)"
1.250 -      by (intro tendsto_dist tendsto_const Lim_at_within tendsto_ident_at)
1.251 +      by (intro tendsto_dist tendsto_const tendsto_ident_at)
1.253    thus "continuous_on s (dist a)"
1.254      unfolding continuous_on ..
1.255 @@ -5350,7 +5341,7 @@
1.256    assumes "\<And>x. isCont f x" and "open s" shows "open (f -` s)"
1.257  proof -
1.258    from assms(1) have "continuous_on UNIV f"
1.259 -    unfolding isCont_def continuous_on_def within_UNIV by simp
1.260 +    unfolding isCont_def continuous_on_def by simp
1.261    hence "open {x \<in> UNIV. f x \<in> s}"
1.262      using open_UNIV `open s` by (rule continuous_open_preimage)
1.263    thus "open (f -` s)"
1.264 @@ -5508,14 +5499,13 @@
1.265  text{* Limits relative to a union.                                               *}
1.267  lemma eventually_within_Un:
1.268 -  "eventually P (net within (s \<union> t)) \<longleftrightarrow>
1.269 -    eventually P (net within s) \<and> eventually P (net within t)"
1.270 -  unfolding Limits.eventually_within
1.271 +  "eventually P (at x within (s \<union> t)) \<longleftrightarrow> eventually P (at x within s) \<and> eventually P (at x within t)"
1.272 +  unfolding eventually_at_filter
1.273    by (auto elim!: eventually_rev_mp)
1.275  lemma Lim_within_union:
1.276 - "(f ---> l) (net within (s \<union> t)) \<longleftrightarrow>
1.277 -  (f ---> l) (net within s) \<and> (f ---> l) (net within t)"
1.278 + "(f ---> l) (at x within (s \<union> t)) \<longleftrightarrow>
1.279 +  (f ---> l) (at x within s) \<and> (f ---> l) (at x within t)"
1.280    unfolding tendsto_def
1.281    by (auto simp add: eventually_within_Un)