src/HOL/Real_Vector_Spaces.thy
changeset 61976 3a27957ac658
parent 61973 0c7e865fa7cb
child 62049 b0f941e207cf
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Dec 30 11:37:29 2015 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Dec 30 14:05:51 2015 +0100
     1.3 @@ -1727,31 +1727,31 @@
     1.4  
     1.5  subsubsection \<open>Limits of Functions\<close>
     1.6  
     1.7 -lemma LIM_def: "f -- (a::'a::metric_space) --> (L::'b::metric_space) =
     1.8 +lemma LIM_def: "f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space) =
     1.9       (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
    1.10          --> dist (f x) L < r)"
    1.11    unfolding tendsto_iff eventually_at by simp
    1.12  
    1.13  lemma metric_LIM_I:
    1.14    "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
    1.15 -    \<Longrightarrow> f -- (a::'a::metric_space) --> (L::'b::metric_space)"
    1.16 +    \<Longrightarrow> f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space)"
    1.17  by (simp add: LIM_def)
    1.18  
    1.19  lemma metric_LIM_D:
    1.20 -  "\<lbrakk>f -- (a::'a::metric_space) --> (L::'b::metric_space); 0 < r\<rbrakk>
    1.21 +  "\<lbrakk>f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space); 0 < r\<rbrakk>
    1.22      \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r"
    1.23  by (simp add: LIM_def)
    1.24  
    1.25  lemma metric_LIM_imp_LIM:
    1.26 -  assumes f: "f -- a --> (l::'a::metric_space)"
    1.27 +  assumes f: "f \<midarrow>a\<rightarrow> (l::'a::metric_space)"
    1.28    assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
    1.29 -  shows "g -- a --> (m::'b::metric_space)"
    1.30 +  shows "g \<midarrow>a\<rightarrow> (m::'b::metric_space)"
    1.31    by (rule metric_tendsto_imp_tendsto [OF f]) (auto simp add: eventually_at_topological le)
    1.32  
    1.33  lemma metric_LIM_equal2:
    1.34    assumes 1: "0 < R"
    1.35    assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
    1.36 -  shows "g -- a --> l \<Longrightarrow> f -- (a::'a::metric_space) --> l"
    1.37 +  shows "g \<midarrow>a\<rightarrow> l \<Longrightarrow> f \<midarrow>(a::'a::metric_space)\<rightarrow> l"
    1.38  apply (rule topological_tendstoI)
    1.39  apply (drule (2) topological_tendstoD)
    1.40  apply (simp add: eventually_at, safe)
    1.41 @@ -1761,19 +1761,19 @@
    1.42  done
    1.43  
    1.44  lemma metric_LIM_compose2:
    1.45 -  assumes f: "f -- (a::'a::metric_space) --> b"
    1.46 -  assumes g: "g -- b --> c"
    1.47 +  assumes f: "f \<midarrow>(a::'a::metric_space)\<rightarrow> b"
    1.48 +  assumes g: "g \<midarrow>b\<rightarrow> c"
    1.49    assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
    1.50 -  shows "(\<lambda>x. g (f x)) -- a --> c"
    1.51 +  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> c"
    1.52    using inj
    1.53    by (intro tendsto_compose_eventually[OF g f]) (auto simp: eventually_at)
    1.54  
    1.55  lemma metric_isCont_LIM_compose2:
    1.56    fixes f :: "'a :: metric_space \<Rightarrow> _"
    1.57    assumes f [unfolded isCont_def]: "isCont f a"
    1.58 -  assumes g: "g -- f a --> l"
    1.59 +  assumes g: "g \<midarrow>f a\<rightarrow> l"
    1.60    assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
    1.61 -  shows "(\<lambda>x. g (f x)) -- a --> l"
    1.62 +  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> l"
    1.63  by (rule metric_LIM_compose2 [OF f g inj])
    1.64  
    1.65  subsection \<open>Complete metric spaces\<close>