renamed the constant "limit" as it is too "generic"
authorpaulson <lp15@cam.ac.uk>
Thu Mar 07 16:59:12 2019 +0000 (3 months ago ago)
changeset 7005603bc14eab432
parent 70055 11065b70407d
child 70057 b49bd228ac8a
child 70061 fe3c12990893
renamed the constant "limit" as it is too "generic"
src/HOL/Analysis/Abstract_Limits.thy
     1.1 --- a/src/HOL/Analysis/Abstract_Limits.thy	Thu Mar 07 14:08:05 2019 +0000
     1.2 +++ b/src/HOL/Analysis/Abstract_Limits.thy	Thu Mar 07 16:59:12 2019 +0000
     1.3 @@ -44,32 +44,32 @@
     1.4  
     1.5  subsection\<open>Limits in a topological space\<close>
     1.6  
     1.7 -definition limit :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
     1.8 -  "limit X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"
     1.9 +definition limitin :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
    1.10 +  "limitin X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"
    1.11  
    1.12 -lemma limit_euclideanreal_iff [simp]: "limit euclideanreal f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
    1.13 -  by (auto simp: limit_def tendsto_def)
    1.14 +lemma limitin_euclideanreal_iff [simp]: "limitin euclideanreal f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
    1.15 +  by (auto simp: limitin_def tendsto_def)
    1.16  
    1.17 -lemma limit_in_topspace: "limit X f l F \<Longrightarrow> l \<in> topspace X"
    1.18 -  by (simp add: limit_def)
    1.19 +lemma limitin_topspace: "limitin X f l F \<Longrightarrow> l \<in> topspace X"
    1.20 +  by (simp add: limitin_def)
    1.21  
    1.22 -lemma limit_const: "limit X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
    1.23 -  by (simp add: limit_def)
    1.24 +lemma limitin_const: "limitin X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
    1.25 +  by (simp add: limitin_def)
    1.26  
    1.27 -lemma limit_real_const: "limit euclideanreal (\<lambda>a. l) l F"
    1.28 -  by (simp add: limit_def)
    1.29 +lemma limitin_real_const: "limitin euclideanreal (\<lambda>a. l) l F"
    1.30 +  by (simp add: limitin_def)
    1.31  
    1.32 -lemma limit_eventually:
    1.33 -   "\<lbrakk>l \<in> topspace X; eventually (\<lambda>x. f x = l) F\<rbrakk> \<Longrightarrow> limit X f l F"
    1.34 -  by (auto simp: limit_def eventually_mono)
    1.35 +lemma limitin_eventually:
    1.36 +   "\<lbrakk>l \<in> topspace X; eventually (\<lambda>x. f x = l) F\<rbrakk> \<Longrightarrow> limitin X f l F"
    1.37 +  by (auto simp: limitin_def eventually_mono)
    1.38  
    1.39 -lemma limit_subsequence:
    1.40 -   "\<lbrakk>strict_mono r; limit X f l sequentially\<rbrakk> \<Longrightarrow> limit X (f \<circ> r) l sequentially"
    1.41 -  unfolding limit_def using eventually_subseq by fastforce
    1.42 +lemma limitin_subsequence:
    1.43 +   "\<lbrakk>strict_mono r; limitin X f l sequentially\<rbrakk> \<Longrightarrow> limitin X (f \<circ> r) l sequentially"
    1.44 +  unfolding limitin_def using eventually_subseq by fastforce
    1.45  
    1.46 -lemma limit_subtopology:
    1.47 -  "limit (subtopology X S) f l F
    1.48 -   \<longleftrightarrow> l \<in> S \<and> eventually (\<lambda>a. f a \<in> S) F \<and> limit X f l F"  (is "?lhs = ?rhs")
    1.49 +lemma limitin_subtopology:
    1.50 +  "limitin (subtopology X S) f l F
    1.51 +   \<longleftrightarrow> l \<in> S \<and> eventually (\<lambda>a. f a \<in> S) F \<and> limitin X f l F"  (is "?lhs = ?rhs")
    1.52  proof (cases "l \<in> S \<inter> topspace X")
    1.53    case True
    1.54    show ?thesis
    1.55 @@ -77,84 +77,84 @@
    1.56      assume L: ?lhs
    1.57      with True
    1.58      have "\<forall>\<^sub>F b in F. f b \<in> topspace X \<inter> S"
    1.59 -      by (metis (no_types) limit_def openin_topspace topspace_subtopology)
    1.60 +      by (metis (no_types) limitin_def openin_topspace topspace_subtopology)
    1.61      with L show ?rhs
    1.62 -      apply (clarsimp simp add: limit_def eventually_mono topspace_subtopology openin_subtopology_alt)
    1.63 +      apply (clarsimp simp add: limitin_def eventually_mono topspace_subtopology openin_subtopology_alt)
    1.64        apply (drule_tac x="S \<inter> U" in spec, force simp: elim: eventually_mono)
    1.65        done
    1.66    next
    1.67      assume ?rhs
    1.68      then show ?lhs
    1.69        using eventually_elim2
    1.70 -      by (fastforce simp add: limit_def topspace_subtopology openin_subtopology_alt)
    1.71 +      by (fastforce simp add: limitin_def topspace_subtopology openin_subtopology_alt)
    1.72    qed
    1.73 -qed (auto simp: limit_def topspace_subtopology)
    1.74 +qed (auto simp: limitin_def topspace_subtopology)
    1.75  
    1.76  
    1.77 -lemma limit_sequentially:
    1.78 -   "limit X S l sequentially \<longleftrightarrow>
    1.79 +lemma limitin_sequentially:
    1.80 +   "limitin X S l sequentially \<longleftrightarrow>
    1.81       l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> (\<exists>N. \<forall>n. N \<le> n \<longrightarrow> S n \<in> U))"
    1.82 -  by (simp add: limit_def eventually_sequentially)
    1.83 +  by (simp add: limitin_def eventually_sequentially)
    1.84  
    1.85 -lemma limit_sequentially_offset:
    1.86 -   "limit X f l sequentially \<Longrightarrow> limit X (\<lambda>i. f (i + k)) l sequentially"
    1.87 -  unfolding limit_sequentially
    1.88 +lemma limitin_sequentially_offset:
    1.89 +   "limitin X f l sequentially \<Longrightarrow> limitin X (\<lambda>i. f (i + k)) l sequentially"
    1.90 +  unfolding limitin_sequentially
    1.91    by (metis add.commute le_add2 order_trans)
    1.92  
    1.93 -lemma limit_sequentially_offset_rev:
    1.94 -  assumes "limit X (\<lambda>i. f (i + k)) l sequentially"
    1.95 -  shows "limit X f l sequentially"
    1.96 +lemma limitin_sequentially_offset_rev:
    1.97 +  assumes "limitin X (\<lambda>i. f (i + k)) l sequentially"
    1.98 +  shows "limitin X f l sequentially"
    1.99  proof -
   1.100    have "\<exists>N. \<forall>n\<ge>N. f n \<in> U" if U: "openin X U" "l \<in> U" for U
   1.101    proof -
   1.102      obtain N where "\<And>n. n\<ge>N \<Longrightarrow> f (n + k) \<in> U"
   1.103 -      using assms U unfolding limit_sequentially by blast
   1.104 +      using assms U unfolding limitin_sequentially by blast
   1.105      then have "\<forall>n\<ge>N+k. f n \<in> U"
   1.106        by (metis add_leD2 le_add_diff_inverse ordered_cancel_comm_monoid_diff_class.le_diff_conv2 add.commute)
   1.107      then show ?thesis ..
   1.108    qed
   1.109    with assms show ?thesis
   1.110 -    unfolding limit_sequentially
   1.111 +    unfolding limitin_sequentially
   1.112      by simp
   1.113  qed
   1.114  
   1.115 -lemma limit_atin:
   1.116 -   "limit Y f y (atin X x) \<longleftrightarrow>
   1.117 +lemma limitin_atin:
   1.118 +   "limitin Y f y (atin X x) \<longleftrightarrow>
   1.119          y \<in> topspace Y \<and>
   1.120          (x \<in> topspace X
   1.121          \<longrightarrow> (\<forall>V. openin Y V \<and> y \<in> V
   1.122                   \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> f ` (U - {x}) \<subseteq> V)))"
   1.123 -  by (auto simp: limit_def eventually_atin image_subset_iff)
   1.124 +  by (auto simp: limitin_def eventually_atin image_subset_iff)
   1.125  
   1.126 -lemma limit_atin_self:
   1.127 -   "limit Y f (f a) (atin X a) \<longleftrightarrow>
   1.128 +lemma limitin_atin_self:
   1.129 +   "limitin Y f (f a) (atin X a) \<longleftrightarrow>
   1.130          f a \<in> topspace Y \<and>
   1.131          (a \<in> topspace X
   1.132           \<longrightarrow> (\<forall>V. openin Y V \<and> f a \<in> V
   1.133                    \<longrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> f ` U \<subseteq> V)))"
   1.134 -  unfolding limit_atin by fastforce
   1.135 +  unfolding limitin_atin by fastforce
   1.136  
   1.137 -lemma limit_trivial:
   1.138 -   "\<lbrakk>trivial_limit F; y \<in> topspace X\<rbrakk> \<Longrightarrow> limit X f y F"
   1.139 -  by (simp add: limit_def)
   1.140 +lemma limitin_trivial:
   1.141 +   "\<lbrakk>trivial_limit F; y \<in> topspace X\<rbrakk> \<Longrightarrow> limitin X f y F"
   1.142 +  by (simp add: limitin_def)
   1.143  
   1.144 -lemma limit_transform_eventually:
   1.145 -   "\<lbrakk>eventually (\<lambda>x. f x = g x) F; limit X f l F\<rbrakk> \<Longrightarrow> limit X g l F"
   1.146 -  unfolding limit_def using eventually_elim2 by fastforce
   1.147 +lemma limitin_transform_eventually:
   1.148 +   "\<lbrakk>eventually (\<lambda>x. f x = g x) F; limitin X f l F\<rbrakk> \<Longrightarrow> limitin X g l F"
   1.149 +  unfolding limitin_def using eventually_elim2 by fastforce
   1.150  
   1.151  lemma continuous_map_limit:
   1.152 -  assumes "continuous_map X Y g" and f: "limit X f l F"
   1.153 -  shows "limit Y (g \<circ> f) (g l) F"
   1.154 +  assumes "continuous_map X Y g" and f: "limitin X f l F"
   1.155 +  shows "limitin Y (g \<circ> f) (g l) F"
   1.156  proof -
   1.157    have "g l \<in> topspace Y"
   1.158 -    by (meson assms continuous_map_def limit_in_topspace)
   1.159 +    by (meson assms continuous_map_def limitin_topspace)
   1.160    moreover
   1.161    have "\<And>U. \<lbrakk>\<forall>V. openin X V \<and> l \<in> V \<longrightarrow> (\<forall>\<^sub>F x in F. f x \<in> V); openin Y U; g l \<in> U\<rbrakk>
   1.162              \<Longrightarrow> \<forall>\<^sub>F x in F. g (f x) \<in> U"
   1.163      using assms eventually_mono
   1.164 -    by (fastforce simp: limit_def dest!: openin_continuous_map_preimage)
   1.165 +    by (fastforce simp: limitin_def dest!: openin_continuous_map_preimage)
   1.166    ultimately show ?thesis
   1.167 -    using f by (fastforce simp add: limit_def)
   1.168 +    using f by (fastforce simp add: limitin_def)
   1.169  qed
   1.170  
   1.171  
   1.172 @@ -171,9 +171,9 @@
   1.173     "topcontinuous_at X Y f x \<longleftrightarrow>
   1.174          x \<in> topspace X \<and>
   1.175          (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
   1.176 -        limit Y f (f x) (atin X x)"
   1.177 +        limitin Y f (f x) (atin X x)"
   1.178    unfolding topcontinuous_at_def
   1.179 -  by (fastforce simp add: limit_atin)+
   1.180 +  by (fastforce simp add: limitin_atin)+
   1.181  
   1.182  lemma continuous_map_eq_topcontinuous_at:
   1.183     "continuous_map X Y f \<longleftrightarrow> (\<forall>x \<in> topspace X. topcontinuous_at X Y f x)"
   1.184 @@ -193,11 +193,11 @@
   1.185  qed
   1.186  
   1.187  lemma continuous_map_atin:
   1.188 -   "continuous_map X Y f \<longleftrightarrow> (\<forall>x \<in> topspace X. limit Y f (f x) (atin X x))"
   1.189 -  by (auto simp: limit_def topcontinuous_at_atin continuous_map_eq_topcontinuous_at)
   1.190 +   "continuous_map X Y f \<longleftrightarrow> (\<forall>x \<in> topspace X. limitin Y f (f x) (atin X x))"
   1.191 +  by (auto simp: limitin_def topcontinuous_at_atin continuous_map_eq_topcontinuous_at)
   1.192  
   1.193 -lemma limit_continuous_map:
   1.194 -   "\<lbrakk>continuous_map X Y f; a \<in> topspace X; f a = b\<rbrakk> \<Longrightarrow> limit Y f b (atin X a)"
   1.195 +lemma limitin_continuous_map:
   1.196 +   "\<lbrakk>continuous_map X Y f; a \<in> topspace X; f a = b\<rbrakk> \<Longrightarrow> limitin Y f b (atin X a)"
   1.197    by (auto simp: continuous_map_atin)
   1.198  
   1.199