src/HOL/Library/Product_Vector.thy
changeset 36661 0a5b7b818d65
parent 36660 1cc4ab4b7ff7
child 37678 0040bafffdef
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Tue May 04 10:06:05 2010 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue May 04 10:42:47 2010 -0700
     1.3 @@ -312,18 +312,6 @@
     1.4         (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
     1.5  qed
     1.6  
     1.7 -lemma LIM_fst: "f -- x --> a \<Longrightarrow> (\<lambda>x. fst (f x)) -- x --> fst a"
     1.8 -unfolding LIM_conv_tendsto by (rule tendsto_fst)
     1.9 -
    1.10 -lemma LIM_snd: "f -- x --> a \<Longrightarrow> (\<lambda>x. snd (f x)) -- x --> snd a"
    1.11 -unfolding LIM_conv_tendsto by (rule tendsto_snd)
    1.12 -
    1.13 -lemma LIM_Pair:
    1.14 -  assumes "f -- x --> a" and "g -- x --> b"
    1.15 -  shows "(\<lambda>x. (f x, g x)) -- x --> (a, b)"
    1.16 -using assms unfolding LIM_conv_tendsto
    1.17 -by (rule tendsto_Pair)
    1.18 -
    1.19  lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
    1.20  unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
    1.21  
    1.22 @@ -348,7 +336,7 @@
    1.23  
    1.24  lemma isCont_Pair [simp]:
    1.25    "\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x"
    1.26 -  unfolding isCont_def by (rule LIM_Pair)
    1.27 +  unfolding isCont_def by (rule tendsto_Pair)
    1.28  
    1.29  subsection {* Product is a complete metric space *}
    1.30