--- 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 *}
--- 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