author huffman Sun Jun 07 15:18:52 2009 -0700 (2009-06-07) changeset 31491 f7310185481d parent 31490 c350f3ad6b0d child 31492 5400beeddb55
generalize tendsto lemmas for products
```     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"
```