src/HOL/Library/Product_Vector.thy
changeset 44233 aa74ce315bae
parent 44214 1e0414bda9af
child 44282 f0de18b62d63
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Tue Aug 16 13:07:52 2011 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue Aug 16 09:31:23 2011 -0700
     1.3 @@ -359,6 +359,16 @@
     1.4         (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
     1.5  qed
     1.6  
     1.7 +lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
     1.8 +  unfolding isCont_def by (rule tendsto_fst)
     1.9 +
    1.10 +lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
    1.11 +  unfolding isCont_def by (rule tendsto_snd)
    1.12 +
    1.13 +lemma isCont_Pair [simp]:
    1.14 +  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
    1.15 +  unfolding isCont_def by (rule tendsto_Pair)
    1.16 +
    1.17  lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
    1.18  unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
    1.19  
    1.20 @@ -381,10 +391,6 @@
    1.21    then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
    1.22  qed
    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 tendsto_Pair)
    1.27 -
    1.28  subsection {* Product is a complete metric space *}
    1.29  
    1.30  instance prod :: (complete_space, complete_space) complete_space