src/HOL/Topological_Spaces.thy
changeset 61973 0c7e865fa7cb
parent 61969 e01015e49041
child 61976 3a27957ac658
     1.1 --- a/src/HOL/Topological_Spaces.thy	Tue Dec 29 23:50:44 2015 +0100
     1.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Dec 30 11:21:54 2015 +0100
     1.3 @@ -480,13 +480,13 @@
     1.4  subsubsection \<open>Tendsto\<close>
     1.5  
     1.6  abbreviation (in topological_space)
     1.7 -  tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "--->" 55) where
     1.8 -  "(f ---> l) F \<equiv> filterlim f (nhds l) F"
     1.9 +  tendsto :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" (infixr "\<longlongrightarrow>" 55) where
    1.10 +  "(f \<longlongrightarrow> l) F \<equiv> filterlim f (nhds l) F"
    1.11  
    1.12  definition (in t2_space) Lim :: "'f filter \<Rightarrow> ('f \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.13 -  "Lim A f = (THE l. (f ---> l) A)"
    1.14 +  "Lim A f = (THE l. (f \<longlongrightarrow> l) A)"
    1.15  
    1.16 -lemma tendsto_eq_rhs: "(f ---> x) F \<Longrightarrow> x = y \<Longrightarrow> (f ---> y) F"
    1.17 +lemma tendsto_eq_rhs: "(f \<longlongrightarrow> x) F \<Longrightarrow> x = y \<Longrightarrow> (f \<longlongrightarrow> y) F"
    1.18    by simp
    1.19  
    1.20  named_theorems tendsto_intros "introduction rules for tendsto"
    1.21 @@ -498,55 +498,55 @@
    1.22  \<close>
    1.23  
    1.24  lemma (in topological_space) tendsto_def:
    1.25 -   "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
    1.26 +   "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
    1.27     unfolding nhds_def filterlim_INF filterlim_principal by auto
    1.28  
    1.29  lemma tendsto_cong:
    1.30    assumes "eventually (\<lambda>x. f x = g x) F"
    1.31 -  shows   "(f ---> c) F \<longleftrightarrow> (g ---> c) F"
    1.32 +  shows   "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) F"
    1.33    by (rule filterlim_cong[OF refl refl assms])
    1.34  
    1.35  
    1.36 -lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
    1.37 +lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f \<longlongrightarrow> l) F' \<Longrightarrow> (f \<longlongrightarrow> l) F"
    1.38    unfolding tendsto_def le_filter_def by fast
    1.39  
    1.40 -lemma tendsto_within_subset: "(f ---> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (at x within T)"
    1.41 +lemma tendsto_within_subset: "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
    1.42    by (blast intro: tendsto_mono at_le)
    1.43  
    1.44  lemma filterlim_at:
    1.45 -  "(LIM x F. f x :> at b within s) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f ---> b) F)"
    1.46 +  "(LIM x F. f x :> at b within s) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> s \<and> f x \<noteq> b) F \<and> (f \<longlongrightarrow> b) F)"
    1.47    by (simp add: at_within_def filterlim_inf filterlim_principal conj_commute)
    1.48  
    1.49  lemma (in topological_space) topological_tendstoI:
    1.50 -  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f ---> l) F"
    1.51 +  "(\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
    1.52    unfolding tendsto_def by auto
    1.53  
    1.54  lemma (in topological_space) topological_tendstoD:
    1.55 -  "(f ---> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
    1.56 +  "(f \<longlongrightarrow> l) F \<Longrightarrow> open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
    1.57    unfolding tendsto_def by auto
    1.58  
    1.59  lemma (in order_topology) order_tendsto_iff:
    1.60 -  "(f ---> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
    1.61 +  "(f \<longlongrightarrow> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
    1.62    unfolding nhds_order filterlim_inf filterlim_INF filterlim_principal by auto
    1.63  
    1.64  lemma (in order_topology) order_tendstoI:
    1.65    "(\<And>a. a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F) \<Longrightarrow> (\<And>a. y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F) \<Longrightarrow>
    1.66 -    (f ---> y) F"
    1.67 +    (f \<longlongrightarrow> y) F"
    1.68    unfolding order_tendsto_iff by auto
    1.69  
    1.70  lemma (in order_topology) order_tendstoD:
    1.71 -  assumes "(f ---> y) F"
    1.72 +  assumes "(f \<longlongrightarrow> y) F"
    1.73    shows "a < y \<Longrightarrow> eventually (\<lambda>x. a < f x) F"
    1.74      and "y < a \<Longrightarrow> eventually (\<lambda>x. f x < a) F"
    1.75    using assms unfolding order_tendsto_iff by auto
    1.76  
    1.77 -lemma tendsto_bot [simp]: "(f ---> a) bot"
    1.78 +lemma tendsto_bot [simp]: "(f \<longlongrightarrow> a) bot"
    1.79    unfolding tendsto_def by simp
    1.80  
    1.81  lemma (in linorder_topology) tendsto_max:
    1.82 -  assumes X: "(X ---> x) net"
    1.83 -  assumes Y: "(Y ---> y) net"
    1.84 -  shows "((\<lambda>x. max (X x) (Y x)) ---> max x y) net"
    1.85 +  assumes X: "(X \<longlongrightarrow> x) net"
    1.86 +  assumes Y: "(Y \<longlongrightarrow> y) net"
    1.87 +  shows "((\<lambda>x. max (X x) (Y x)) \<longlongrightarrow> max x y) net"
    1.88  proof (rule order_tendstoI)
    1.89    fix a assume "a < max x y"
    1.90    then show "eventually (\<lambda>x. a < max (X x) (Y x)) net"
    1.91 @@ -560,9 +560,9 @@
    1.92  qed
    1.93  
    1.94  lemma (in linorder_topology) tendsto_min:
    1.95 -  assumes X: "(X ---> x) net"
    1.96 -  assumes Y: "(Y ---> y) net"
    1.97 -  shows "((\<lambda>x. min (X x) (Y x)) ---> min x y) net"
    1.98 +  assumes X: "(X \<longlongrightarrow> x) net"
    1.99 +  assumes Y: "(Y \<longlongrightarrow> y) net"
   1.100 +  shows "((\<lambda>x. min (X x) (Y x)) \<longlongrightarrow> min x y) net"
   1.101  proof (rule order_tendstoI)
   1.102    fix a assume "a < min x y"
   1.103    then show "eventually (\<lambda>x. a < min (X x) (Y x)) net"
   1.104 @@ -575,24 +575,24 @@
   1.105      by (auto simp: min_less_iff_disj elim: eventually_mono)
   1.106  qed
   1.107  
   1.108 -lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) ---> a) (at a within s)"
   1.109 +lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) \<longlongrightarrow> a) (at a within s)"
   1.110    unfolding tendsto_def eventually_at_topological by auto
   1.111  
   1.112 -lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) ---> k) F"
   1.113 +lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) \<longlongrightarrow> k) F"
   1.114    by (simp add: tendsto_def)
   1.115  
   1.116  lemma (in t2_space) tendsto_unique:
   1.117 -  assumes "F \<noteq> bot" and "(f ---> a) F" and "(f ---> b) F"
   1.118 +  assumes "F \<noteq> bot" and "(f \<longlongrightarrow> a) F" and "(f \<longlongrightarrow> b) F"
   1.119    shows "a = b"
   1.120  proof (rule ccontr)
   1.121    assume "a \<noteq> b"
   1.122    obtain U V where "open U" "open V" "a \<in> U" "b \<in> V" "U \<inter> V = {}"
   1.123      using hausdorff [OF \<open>a \<noteq> b\<close>] by fast
   1.124    have "eventually (\<lambda>x. f x \<in> U) F"
   1.125 -    using \<open>(f ---> a) F\<close> \<open>open U\<close> \<open>a \<in> U\<close> by (rule topological_tendstoD)
   1.126 +    using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open U\<close> \<open>a \<in> U\<close> by (rule topological_tendstoD)
   1.127    moreover
   1.128    have "eventually (\<lambda>x. f x \<in> V) F"
   1.129 -    using \<open>(f ---> b) F\<close> \<open>open V\<close> \<open>b \<in> V\<close> by (rule topological_tendstoD)
   1.130 +    using \<open>(f \<longlongrightarrow> b) F\<close> \<open>open V\<close> \<open>b \<in> V\<close> by (rule topological_tendstoD)
   1.131    ultimately
   1.132    have "eventually (\<lambda>x. False) F"
   1.133    proof eventually_elim
   1.134 @@ -605,28 +605,28 @@
   1.135  qed
   1.136  
   1.137  lemma (in t2_space) tendsto_const_iff:
   1.138 -  assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) ---> b) F \<longleftrightarrow> a = b"
   1.139 +  assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) \<longlongrightarrow> b) F \<longleftrightarrow> a = b"
   1.140    by (auto intro!: tendsto_unique [OF assms tendsto_const])
   1.141  
   1.142  lemma increasing_tendsto:
   1.143    fixes f :: "_ \<Rightarrow> 'a::order_topology"
   1.144    assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
   1.145        and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
   1.146 -  shows "(f ---> l) F"
   1.147 +  shows "(f \<longlongrightarrow> l) F"
   1.148    using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
   1.149  
   1.150  lemma decreasing_tendsto:
   1.151    fixes f :: "_ \<Rightarrow> 'a::order_topology"
   1.152    assumes bdd: "eventually (\<lambda>n. l \<le> f n) F"
   1.153        and en: "\<And>x. l < x \<Longrightarrow> eventually (\<lambda>n. f n < x) F"
   1.154 -  shows "(f ---> l) F"
   1.155 +  shows "(f \<longlongrightarrow> l) F"
   1.156    using assms by (intro order_tendstoI) (auto elim!: eventually_mono)
   1.157  
   1.158  lemma tendsto_sandwich:
   1.159    fixes f g h :: "'a \<Rightarrow> 'b::order_topology"
   1.160    assumes ev: "eventually (\<lambda>n. f n \<le> g n) net" "eventually (\<lambda>n. g n \<le> h n) net"
   1.161 -  assumes lim: "(f ---> c) net" "(h ---> c) net"
   1.162 -  shows "(g ---> c) net"
   1.163 +  assumes lim: "(f \<longlongrightarrow> c) net" "(h \<longlongrightarrow> c) net"
   1.164 +  shows "(g \<longlongrightarrow> c) net"
   1.165  proof (rule order_tendstoI)
   1.166    fix a show "a < c \<Longrightarrow> eventually (\<lambda>x. a < g x) net"
   1.167      using order_tendstoD[OF lim(1), of a] ev by (auto elim: eventually_elim2)
   1.168 @@ -638,7 +638,7 @@
   1.169  lemma limit_frequently_eq:
   1.170    assumes "F \<noteq> bot"
   1.171    assumes "frequently (\<lambda>x. f x = c) F"
   1.172 -  assumes "(f ---> d) F"
   1.173 +  assumes "(f \<longlongrightarrow> d) F"
   1.174    shows   "d = (c :: 'a :: t1_space)"
   1.175  proof (rule ccontr)
   1.176    assume "d \<noteq> c"
   1.177 @@ -649,7 +649,7 @@
   1.178  qed
   1.179  
   1.180  lemma tendsto_imp_eventually_ne:
   1.181 -  assumes "F \<noteq> bot" "(f ---> c) F" "c \<noteq> (c' :: 'a :: t1_space)"
   1.182 +  assumes "F \<noteq> bot" "(f \<longlongrightarrow> c) F" "c \<noteq> (c' :: 'a :: t1_space)"
   1.183    shows   "eventually (\<lambda>z. f z \<noteq> c') F"
   1.184  proof (rule ccontr)
   1.185    assume "\<not>eventually (\<lambda>z. f z \<noteq> c') F"
   1.186 @@ -660,7 +660,7 @@
   1.187  lemma tendsto_le:
   1.188    fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
   1.189    assumes F: "\<not> trivial_limit F"
   1.190 -  assumes x: "(f ---> x) F" and y: "(g ---> y) F"
   1.191 +  assumes x: "(f \<longlongrightarrow> x) F" and y: "(g \<longlongrightarrow> y) F"
   1.192    assumes ev: "eventually (\<lambda>x. g x \<le> f x) F"
   1.193    shows "y \<le> x"
   1.194  proof (rule ccontr)
   1.195 @@ -678,14 +678,14 @@
   1.196  lemma tendsto_le_const:
   1.197    fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
   1.198    assumes F: "\<not> trivial_limit F"
   1.199 -  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>i. a \<le> f i) F"
   1.200 +  assumes x: "(f \<longlongrightarrow> x) F" and a: "eventually (\<lambda>i. a \<le> f i) F"
   1.201    shows "a \<le> x"
   1.202    using F x tendsto_const a by (rule tendsto_le)
   1.203  
   1.204  lemma tendsto_ge_const:
   1.205    fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
   1.206    assumes F: "\<not> trivial_limit F"
   1.207 -  assumes x: "(f ---> x) F" and a: "eventually (\<lambda>i. a \<ge> f i) F"
   1.208 +  assumes x: "(f \<longlongrightarrow> x) F" and a: "eventually (\<lambda>i. a \<ge> f i) F"
   1.209    shows "a \<ge> x"
   1.210    by (rule tendsto_le [OF F tendsto_const x a])
   1.211  
   1.212 @@ -695,7 +695,7 @@
   1.213  subsubsection \<open>Rules about @{const Lim}\<close>
   1.214  
   1.215  lemma tendsto_Lim:
   1.216 -  "\<not>(trivial_limit net) \<Longrightarrow> (f ---> l) net \<Longrightarrow> Lim net f = l"
   1.217 +  "\<not>(trivial_limit net) \<Longrightarrow> (f \<longlongrightarrow> l) net \<Longrightarrow> Lim net f = l"
   1.218    unfolding Lim_def using tendsto_unique[of net f] by auto
   1.219  
   1.220  lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
   1.221 @@ -771,7 +771,7 @@
   1.222  qed
   1.223  
   1.224  lemma tendsto_at_within_iff_tendsto_nhds:
   1.225 -  "(g ---> g l) (at l within S) \<longleftrightarrow> (g ---> g l) (inf (nhds l) (principal S))"
   1.226 +  "(g \<longlongrightarrow> g l) (at l within S) \<longleftrightarrow> (g \<longlongrightarrow> g l) (inf (nhds l) (principal S))"
   1.227    unfolding tendsto_def eventually_at_filter eventually_inf_principal
   1.228    by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
   1.229  
   1.230 @@ -780,7 +780,7 @@
   1.231  abbreviation (in topological_space)
   1.232    LIMSEQ :: "[nat \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
   1.233      ("((_)/ \<longlonglongrightarrow> (_))" [60, 60] 60) where
   1.234 -  "X \<longlonglongrightarrow> L \<equiv> (X ---> L) sequentially"
   1.235 +  "X \<longlonglongrightarrow> L \<equiv> (X \<longlongrightarrow> L) sequentially"
   1.236  
   1.237  abbreviation (in t2_space) lim :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a" where
   1.238    "lim X \<equiv> Lim sequentially X"
   1.239 @@ -1196,7 +1196,7 @@
   1.240  
   1.241  lemma tendsto_at_iff_sequentially:
   1.242    fixes f :: "'a :: first_countable_topology \<Rightarrow> _"
   1.243 -  shows "(f ---> a) (at x within s) \<longleftrightarrow> (\<forall>X. (\<forall>i. X i \<in> s - {x}) \<longrightarrow> X \<longlonglongrightarrow> x \<longrightarrow> ((f \<circ> X) \<longlonglongrightarrow> a))"
   1.244 +  shows "(f \<longlongrightarrow> a) (at x within s) \<longleftrightarrow> (\<forall>X. (\<forall>i. X i \<in> s - {x}) \<longrightarrow> X \<longlonglongrightarrow> x \<longrightarrow> ((f \<circ> X) \<longlonglongrightarrow> a))"
   1.245    unfolding filterlim_def[of _ "nhds a"] le_filter_def eventually_filtermap at_within_def eventually_nhds_within_iff_sequentially comp_def
   1.246    by metis
   1.247  
   1.248 @@ -1205,9 +1205,9 @@
   1.249  abbreviation
   1.250    LIM :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   1.251          ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
   1.252 -  "f -- a --> L \<equiv> (f ---> L) (at a)"
   1.253 +  "f -- a --> L \<equiv> (f \<longlongrightarrow> L) (at a)"
   1.254  
   1.255 -lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
   1.256 +lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
   1.257    unfolding tendsto_def by (simp add: at_within_open[where S=S])
   1.258  
   1.259  lemma LIM_const_not_eq[tendsto_intros]:
   1.260 @@ -1241,19 +1241,19 @@
   1.261    by simp
   1.262  
   1.263  lemma tendsto_at_iff_tendsto_nhds:
   1.264 -  "g -- l --> g l \<longleftrightarrow> (g ---> g l) (nhds l)"
   1.265 +  "g -- l --> g l \<longleftrightarrow> (g \<longlongrightarrow> g l) (nhds l)"
   1.266    unfolding tendsto_def eventually_at_filter
   1.267    by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
   1.268  
   1.269  lemma tendsto_compose:
   1.270 -  "g -- l --> g l \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
   1.271 +  "g -- l --> g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
   1.272    unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
   1.273  
   1.274  lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
   1.275    unfolding o_def by (rule tendsto_compose)
   1.276  
   1.277  lemma tendsto_compose_eventually:
   1.278 -  "g -- l --> m \<Longrightarrow> (f ---> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> m) F"
   1.279 +  "g -- l --> m \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> m) F"
   1.280    by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)
   1.281  
   1.282  lemma LIM_compose_eventually:
   1.283 @@ -1263,7 +1263,7 @@
   1.284    shows "(\<lambda>x. g (f x)) -- a --> c"
   1.285    using g f inj by (rule tendsto_compose_eventually)
   1.286  
   1.287 -lemma tendsto_compose_filtermap: "((g \<circ> f) ---> T) F \<longleftrightarrow> (g ---> T) (filtermap f F)"
   1.288 +lemma tendsto_compose_filtermap: "((g \<circ> f) \<longlongrightarrow> T) F \<longleftrightarrow> (g \<longlongrightarrow> T) (filtermap f F)"
   1.289    by (simp add: filterlim_def filtermap_filtermap comp_def)
   1.290  
   1.291  subsubsection \<open>Relation of LIM and LIMSEQ\<close>
   1.292 @@ -1329,7 +1329,7 @@
   1.293    fixes a :: "_ :: {linorder_topology, first_countable_topology}"
   1.294    assumes "b < a"
   1.295    assumes *: "\<And>S. (\<And>n. S n < a) \<Longrightarrow> (\<And>n. b < S n) \<Longrightarrow> incseq S \<Longrightarrow> S \<longlonglongrightarrow> a \<Longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L"
   1.296 -  shows "(X ---> L) (at_left a)"
   1.297 +  shows "(X \<longlongrightarrow> L) (at_left a)"
   1.298    using assms unfolding tendsto_def [where l=L]
   1.299    by (simp add: sequentially_imp_eventually_at_left)
   1.300  
   1.301 @@ -1367,7 +1367,7 @@
   1.302    fixes a :: "_ :: {linorder_topology, first_countable_topology}"
   1.303    assumes "a < b"
   1.304    assumes *: "\<And>S. (\<And>n. a < S n) \<Longrightarrow> (\<And>n. S n < b) \<Longrightarrow> decseq S \<Longrightarrow> S \<longlonglongrightarrow> a \<Longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L"
   1.305 -  shows "(X ---> L) (at_right a)"
   1.306 +  shows "(X \<longlongrightarrow> L) (at_right a)"
   1.307    using assms unfolding tendsto_def [where l=L]
   1.308    by (simp add: sequentially_imp_eventually_at_right)
   1.309  
   1.310 @@ -1376,7 +1376,7 @@
   1.311  subsubsection \<open>Continuity on a set\<close>
   1.312  
   1.313  definition continuous_on :: "'a set \<Rightarrow> ('a :: topological_space \<Rightarrow> 'b :: topological_space) \<Rightarrow> bool" where
   1.314 -  "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
   1.315 +  "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f \<longlongrightarrow> f x) (at x within s))"
   1.316  
   1.317  lemma continuous_on_cong [cong]:
   1.318    "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
   1.319 @@ -1559,7 +1559,7 @@
   1.320  subsubsection \<open>Continuity at a point\<close>
   1.321  
   1.322  definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
   1.323 -  "continuous F f \<longleftrightarrow> (f ---> f (Lim F (\<lambda>x. x))) F"
   1.324 +  "continuous F f \<longleftrightarrow> (f \<longlongrightarrow> f (Lim F (\<lambda>x. x))) F"
   1.325  
   1.326  lemma continuous_bot[continuous_intros, simp]: "continuous bot f"
   1.327    unfolding continuous_def by auto
   1.328 @@ -1567,7 +1567,7 @@
   1.329  lemma continuous_trivial_limit: "trivial_limit net \<Longrightarrow> continuous net f"
   1.330    by simp
   1.331  
   1.332 -lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f x) (at x within s)"
   1.333 +lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f \<longlongrightarrow> f x) (at x within s)"
   1.334    by (cases "trivial_limit (at x within s)") (auto simp add: Lim_ident_at continuous_def)
   1.335  
   1.336  lemma continuous_within_topological:
   1.337 @@ -1619,7 +1619,7 @@
   1.338  lemma isCont_o[continuous_intros]: "isCont f a \<Longrightarrow> isCont g (f a) \<Longrightarrow> isCont (g \<circ> f) a"
   1.339    unfolding o_def by (rule isCont_o2)
   1.340  
   1.341 -lemma isCont_tendsto_compose: "isCont g l \<Longrightarrow> (f ---> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) ---> g l) F"
   1.342 +lemma isCont_tendsto_compose: "isCont g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
   1.343    unfolding isCont_def by (rule tendsto_compose)
   1.344  
   1.345  lemma continuous_within_compose3:
   1.346 @@ -2271,7 +2271,7 @@
   1.347    assumes S: "S \<noteq> {}" "bdd_above S"
   1.348    shows "f (Sup S) = (SUP s:S. f s)"
   1.349  proof (rule antisym)
   1.350 -  have f: "(f ---> f (Sup S)) (at_left (Sup S))"
   1.351 +  have f: "(f \<longlongrightarrow> f (Sup S)) (at_left (Sup S))"
   1.352      using cont unfolding continuous_within .
   1.353  
   1.354    show "f (Sup S) \<le> (SUP s:S. f s)"
   1.355 @@ -2308,7 +2308,7 @@
   1.356    assumes S: "S \<noteq> {}" "bdd_above S"
   1.357    shows "f (Sup S) = (INF s:S. f s)"
   1.358  proof (rule antisym)
   1.359 -  have f: "(f ---> f (Sup S)) (at_left (Sup S))"
   1.360 +  have f: "(f \<longlongrightarrow> f (Sup S)) (at_left (Sup S))"
   1.361      using cont unfolding continuous_within .
   1.362  
   1.363    show "(INF s:S. f s) \<le> f (Sup S)"
   1.364 @@ -2345,7 +2345,7 @@
   1.365    assumes S: "S \<noteq> {}" "bdd_below S"
   1.366    shows "f (Inf S) = (INF s:S. f s)"
   1.367  proof (rule antisym)
   1.368 -  have f: "(f ---> f (Inf S)) (at_right (Inf S))"
   1.369 +  have f: "(f \<longlongrightarrow> f (Inf S)) (at_right (Inf S))"
   1.370      using cont unfolding continuous_within .
   1.371  
   1.372    show "(INF s:S. f s) \<le> f (Inf S)"
   1.373 @@ -2382,7 +2382,7 @@
   1.374    assumes S: "S \<noteq> {}" "bdd_below S"
   1.375    shows "f (Inf S) = (SUP s:S. f s)"
   1.376  proof (rule antisym)
   1.377 -  have f: "(f ---> f (Inf S)) (at_right (Inf S))"
   1.378 +  have f: "(f \<longlongrightarrow> f (Inf S)) (at_right (Inf S))"
   1.379      using cont unfolding continuous_within .
   1.380  
   1.381    show "f (Inf S) \<le> (SUP s:S. f s)"