src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy

   thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}"
     by (simp add: closed_INT closed_vimage_vec_nth)
 qed
 
 lemma tendsto_vec_nth [tendsto_intros]:
-  assumes "((\<lambda>x. f x) ---> a) net"
-  shows "((\<lambda>x. f x $ i) ---> a $ i) net"
+  assumes "((\<lambda>x. f x) \<longlongrightarrow> a) net"
+  shows "((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
 proof (rule topological_tendstoI)
   fix S assume "open S" "a $ i \<in> S"
   then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)"
     by (simp_all add: open_vimage_vec_nth)
   with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net"

 
 lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
   unfolding isCont_def by (rule tendsto_vec_nth)
 
 lemma vec_tendstoI:
-  assumes "\<And>i. ((\<lambda>x. f x $ i) ---> a $ i) net"
-  shows "((\<lambda>x. f x) ---> a) net"
+  assumes "\<And>i. ((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net"
+  shows "((\<lambda>x. f x) \<longlongrightarrow> a) net"
 proof (rule topological_tendstoI)
   fix S assume "open S" and "a \<in> S"
   then obtain A where A: "\<And>i. open (A i)" "\<And>i. a $ i \<in> A i"
     and S: "\<And>y. \<forall>i. y $ i \<in> A i \<Longrightarrow> y \<in> S"
     unfolding open_vec_def by metis

   thus "eventually (\<lambda>x. f x \<in> S) net"
     by (rule eventually_mono, simp add: S)
 qed
 
 lemma tendsto_vec_lambda [tendsto_intros]:
-  assumes "\<And>i. ((\<lambda>x. f x i) ---> a i) net"
-  shows "((\<lambda>x. \<chi> i. f x i) ---> (\<chi> i. a i)) net"
+  assumes "\<And>i. ((\<lambda>x. f x i) \<longlongrightarrow> a i) net"
+  shows "((\<lambda>x. \<chi> i. f x i) \<longlongrightarrow> (\<chi> i. a i)) net"
   using assms by (simp add: vec_tendstoI)
 
 lemma open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)"
 proof (rule openI)
   fix a assume "a \<in> (\<lambda>x. x $ i) ` S"