src/HOL/Library/Product_Vector.thy

 qed
 
 subsubsection \<open>Continuity of operations\<close>
 
 lemma tendsto_fst [tendsto_intros]:
-  assumes "(f ---> a) F"
-  shows "((\<lambda>x. fst (f x)) ---> fst a) F"
+  assumes "(f \<longlongrightarrow> a) F"
+  shows "((\<lambda>x. fst (f x)) \<longlongrightarrow> fst a) F"
 proof (rule topological_tendstoI)
   fix S assume "open S" and "fst a \<in> S"
   then have "open (fst -` S)" and "a \<in> fst -` S"
     by (simp_all add: open_vimage_fst)
   with assms have "eventually (\<lambda>x. f x \<in> fst -` S) F"

   then show "eventually (\<lambda>x. fst (f x) \<in> S) F"
     by simp
 qed
 
 lemma tendsto_snd [tendsto_intros]:
-  assumes "(f ---> a) F"
-  shows "((\<lambda>x. snd (f x)) ---> snd a) F"
+  assumes "(f \<longlongrightarrow> a) F"
+  shows "((\<lambda>x. snd (f x)) \<longlongrightarrow> snd a) F"
 proof (rule topological_tendstoI)
   fix S assume "open S" and "snd a \<in> S"
   then have "open (snd -` S)" and "a \<in> snd -` S"
     by (simp_all add: open_vimage_snd)
   with assms have "eventually (\<lambda>x. f x \<in> snd -` S) F"

   then show "eventually (\<lambda>x. snd (f x) \<in> S) F"
     by simp
 qed
 
 lemma tendsto_Pair [tendsto_intros]:
-  assumes "(f ---> a) F" and "(g ---> b) F"
-  shows "((\<lambda>x. (f x, g x)) ---> (a, b)) F"
+  assumes "(f \<longlongrightarrow> a) F" and "(g \<longlongrightarrow> b) F"
+  shows "((\<lambda>x. (f x, g x)) \<longlongrightarrow> (a, b)) F"
 proof (rule topological_tendstoI)
   fix S assume "open S" and "(a, b) \<in> S"
   then obtain A B where "open A" "open B" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
     unfolding open_prod_def by fast
   have "eventually (\<lambda>x. f x \<in> A) F"
-    using \<open>(f ---> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
+    using \<open>(f \<longlongrightarrow> a) F\<close> \<open>open A\<close> \<open>a \<in> A\<close>
     by (rule topological_tendstoD)
   moreover
   have "eventually (\<lambda>x. g x \<in> B) F"
-    using \<open>(g ---> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
+    using \<open>(g \<longlongrightarrow> b) F\<close> \<open>open B\<close> \<open>b \<in> B\<close>
     by (rule topological_tendstoD)
   ultimately
   show "eventually (\<lambda>x. (f x, g x) \<in> S) F"
     by (rule eventually_elim2)
        (simp add: subsetD [OF \<open>A \<times> B \<subseteq> S\<close>])

     using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
   let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
   let ?Rg = "\<lambda>y. g y - g x - g' (y - x)"
   let ?R = "\<lambda>y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))"
 
-  show "((\<lambda>y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) ---> 0) (at x within s)"
+  show "((\<lambda>y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) \<longlongrightarrow> 0) (at x within s)"
     using f g by (intro tendsto_add_zero) (auto simp: has_derivative_iff_norm)
 
   fix y :: 'a assume "y \<noteq> x"
   show "norm (?R y) / norm (y - x) \<le> norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)"
     unfolding add_divide_distrib [symmetric]