generalize lemma isCont_vec_nth
authorhuffman
Wed Aug 31 10:42:31 2011 -0700 (2011-08-31 ago)
changeset 446316820684c7a58
parent 44630 d08cb39b628a
child 44632 076a45f65e12
generalize lemma isCont_vec_nth
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 31 10:24:29 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 31 10:42:31 2011 -0700
     1.3 @@ -206,6 +206,9 @@
     1.4      by simp
     1.5  qed
     1.6  
     1.7 +lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
     1.8 +  unfolding isCont_def by (rule tendsto_vec_nth)
     1.9 +
    1.10  lemma eventually_Ball_finite: (* TODO: move *)
    1.11    assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
    1.12    shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
    1.13 @@ -435,9 +438,6 @@
    1.14  apply (rule_tac x="1" in exI, simp add: norm_nth_le)
    1.15  done
    1.16  
    1.17 -lemmas isCont_vec_nth [simp] =
    1.18 -  bounded_linear.isCont [OF bounded_linear_vec_nth]
    1.19 -
    1.20  instance vec :: (banach, finite) banach ..
    1.21  
    1.22