src/HOL/Library/Product_Vector.thy
changeset 31565 da5a5589418e
parent 31563 ded2364d14d4
child 31568 963caf6fa234
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Thu Jun 11 10:37:02 2009 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Thu Jun 11 11:51:12 2009 -0700
     1.3 @@ -177,7 +177,7 @@
     1.4  lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
     1.5  unfolding dist_prod_def by simp
     1.6  
     1.7 -lemma tendsto_fst:
     1.8 +lemma tendsto_fst [tendsto_intros]:
     1.9    assumes "(f ---> a) net"
    1.10    shows "((\<lambda>x. fst (f x)) ---> fst a) net"
    1.11  proof (rule topological_tendstoI)
    1.12 @@ -196,7 +196,7 @@
    1.13      by simp
    1.14  qed
    1.15  
    1.16 -lemma tendsto_snd:
    1.17 +lemma tendsto_snd [tendsto_intros]:
    1.18    assumes "(f ---> a) net"
    1.19    shows "((\<lambda>x. snd (f x)) ---> snd a) net"
    1.20  proof (rule topological_tendstoI)
    1.21 @@ -215,7 +215,7 @@
    1.22      by simp
    1.23  qed
    1.24  
    1.25 -lemma tendsto_Pair:
    1.26 +lemma tendsto_Pair [tendsto_intros]:
    1.27    assumes "(f ---> a) net" and "(g ---> b) net"
    1.28    shows "((\<lambda>x. (f x, g x)) ---> (a, b)) net"
    1.29  proof (rule topological_tendstoI)