generalize tendsto lemmas for products
authorhuffman
Sun Jun 07 15:18:52 2009 -0700 (2009-06-07)
changeset 31491f7310185481d
parent 31490 c350f3ad6b0d
child 31492 5400beeddb55
generalize tendsto lemmas for products
src/HOL/Library/Product_Vector.thy
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Sun Jun 07 12:00:03 2009 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Sun Jun 07 15:18:52 2009 -0700
     1.3 @@ -160,45 +160,61 @@
     1.4  unfolding dist_prod_def by simp
     1.5  
     1.6  lemma tendsto_fst:
     1.7 -  assumes "tendsto f a net"
     1.8 -  shows "tendsto (\<lambda>x. fst (f x)) (fst a) net"
     1.9 -proof (rule tendstoI)
    1.10 -  fix r :: real assume "0 < r"
    1.11 -  have "eventually (\<lambda>x. dist (f x) a < r) net"
    1.12 -    using `tendsto f a net` `0 < r` by (rule tendstoD)
    1.13 -  thus "eventually (\<lambda>x. dist (fst (f x)) (fst a) < r) net"
    1.14 -    by (rule eventually_elim1)
    1.15 -       (rule le_less_trans [OF dist_fst_le])
    1.16 +  assumes "(f ---> a) net"
    1.17 +  shows "((\<lambda>x. fst (f x)) ---> fst a) net"
    1.18 +proof (rule topological_tendstoI)
    1.19 +  fix S assume "S \<in> topo" "fst a \<in> S"
    1.20 +  then have "fst -` S \<in> topo" "a \<in> fst -` S"
    1.21 +    unfolding topo_prod_def
    1.22 +    apply simp_all
    1.23 +    apply clarify
    1.24 +    apply (erule rev_bexI, simp)
    1.25 +    apply (rule rev_bexI [OF topo_UNIV])
    1.26 +    apply auto
    1.27 +    done
    1.28 +  with assms have "eventually (\<lambda>x. f x \<in> fst -` S) net"
    1.29 +    by (rule topological_tendstoD)
    1.30 +  then show "eventually (\<lambda>x. fst (f x) \<in> S) net"
    1.31 +    by simp
    1.32  qed
    1.33  
    1.34  lemma tendsto_snd:
    1.35 -  assumes "tendsto f a net"
    1.36 -  shows "tendsto (\<lambda>x. snd (f x)) (snd a) net"
    1.37 -proof (rule tendstoI)
    1.38 -  fix r :: real assume "0 < r"
    1.39 -  have "eventually (\<lambda>x. dist (f x) a < r) net"
    1.40 -    using `tendsto f a net` `0 < r` by (rule tendstoD)
    1.41 -  thus "eventually (\<lambda>x. dist (snd (f x)) (snd a) < r) net"
    1.42 -    by (rule eventually_elim1)
    1.43 -       (rule le_less_trans [OF dist_snd_le])
    1.44 +  assumes "(f ---> a) net"
    1.45 +  shows "((\<lambda>x. snd (f x)) ---> snd a) net"
    1.46 +proof (rule topological_tendstoI)
    1.47 +  fix S assume "S \<in> topo" "snd a \<in> S"
    1.48 +  then have "snd -` S \<in> topo" "a \<in> snd -` S"
    1.49 +    unfolding topo_prod_def
    1.50 +    apply simp_all
    1.51 +    apply clarify
    1.52 +    apply (rule rev_bexI [OF topo_UNIV])
    1.53 +    apply (erule rev_bexI)
    1.54 +    apply auto
    1.55 +    done
    1.56 +  with assms have "eventually (\<lambda>x. f x \<in> snd -` S) net"
    1.57 +    by (rule topological_tendstoD)
    1.58 +  then show "eventually (\<lambda>x. snd (f x) \<in> S) net"
    1.59 +    by simp
    1.60  qed
    1.61  
    1.62  lemma tendsto_Pair:
    1.63 -  assumes "tendsto X a net" and "tendsto Y b net"
    1.64 -  shows "tendsto (\<lambda>i. (X i, Y i)) (a, b) net"
    1.65 -proof (rule tendstoI)
    1.66 -  fix r :: real assume "0 < r"
    1.67 -  then have "0 < r / sqrt 2" (is "0 < ?s")
    1.68 -    by (simp add: divide_pos_pos)
    1.69 -  have "eventually (\<lambda>i. dist (X i) a < ?s) net"
    1.70 -    using `tendsto X a net` `0 < ?s` by (rule tendstoD)
    1.71 +  assumes "(f ---> a) net" and "(g ---> b) net"
    1.72 +  shows "((\<lambda>x. (f x, g x)) ---> (a, b)) net"
    1.73 +proof (rule topological_tendstoI)
    1.74 +  fix S assume "S \<in> topo" "(a, b) \<in> S"
    1.75 +  then obtain A B where "A \<in> topo" "B \<in> topo" "a \<in> A" "b \<in> B" "A \<times> B \<subseteq> S"
    1.76 +    unfolding topo_prod_def by auto
    1.77 +  have "eventually (\<lambda>x. f x \<in> A) net"
    1.78 +    using `(f ---> a) net` `A \<in> topo` `a \<in> A`
    1.79 +    by (rule topological_tendstoD)
    1.80    moreover
    1.81 -  have "eventually (\<lambda>i. dist (Y i) b < ?s) net"
    1.82 -    using `tendsto Y b net` `0 < ?s` by (rule tendstoD)
    1.83 +  have "eventually (\<lambda>x. g x \<in> B) net"
    1.84 +    using `(g ---> b) net` `B \<in> topo` `b \<in> B`
    1.85 +    by (rule topological_tendstoD)
    1.86    ultimately
    1.87 -  show "eventually (\<lambda>i. dist (X i, Y i) (a, b) < r) net"
    1.88 +  show "eventually (\<lambda>x. (f x, g x) \<in> S) net"
    1.89      by (rule eventually_elim2)
    1.90 -       (simp add: real_sqrt_sum_squares_less dist_Pair_Pair)
    1.91 +       (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
    1.92  qed
    1.93  
    1.94  lemma LIMSEQ_fst: "(X ----> a) \<Longrightarrow> (\<lambda>n. fst (X n)) ----> fst a"