# HG changeset patch
# User huffman
# Date 1312920575 25200
# Node ID e6c6ca74d81beb38d2259323d2d51ea78a259210
# Parent  7b57b9295d98c2bc7b7a4306bb0c1d686f4ecc84
bounded_linear interpretation for euclidean_component

diff -r 7b57b9295d98 -r e6c6ca74d81b src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 09 12:50:22 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 09 13:09:35 2011 -0700
@@ -1731,8 +1731,10 @@
 
 end
 
-interpretation euclidean_component: additive "\<lambda>x. euclidean_component x i"
-proof qed (simp add: euclidean_component_def inner_right.add)
+interpretation euclidean_component:
+  bounded_linear "\<lambda>x. euclidean_component x i"
+  unfolding euclidean_component_def
+  by (rule inner.bounded_linear_right)
 
 subsection{* Euclidean Spaces as Typeclass *}
 
diff -r 7b57b9295d98 -r e6c6ca74d81b src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 09 12:50:22 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 09 13:09:35 2011 -0700
@@ -1250,11 +1250,6 @@
     using assms `e>0` unfolding tendsto_iff by auto
 qed
 
-lemma Lim_component: (* TODO: rename and declare [tendsto_intros] *)
-  fixes f :: "'a \<Rightarrow> ('a::euclidean_space)"
-  shows "(f ---> l) net \<Longrightarrow> ((\<lambda>a. f a $$i) ---> l$$i) net"
-  unfolding euclidean_component_def by (intro tendsto_intros)
-
 lemma Lim_transform_bound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
@@ -6115,6 +6110,7 @@
 lemmas Lim_vmul = scaleR.tendsto [OF _ tendsto_const]
 lemmas Lim_null_norm = tendsto_norm_zero_iff [symmetric]
 lemmas Lim_linear = bounded_linear.tendsto [COMP swap_prems_rl]
+lemmas Lim_component = euclidean_component.tendsto
 lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
 
 end