--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Aug 22 10:19:39 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon Aug 22 10:43:10 2011 -0700
@@ -1102,11 +1102,6 @@
lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
by (simp add: Collect_all_eq closed_INT closed_Collect_le)
-lemma Lim_component_cart:
- fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
- shows "(f ---> l) net \<Longrightarrow> ((\<lambda>a. f a $i) ---> l$i) net"
- by (intro tendsto_intros)
-
lemma bounded_component_cart: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x $ i) ` s)"
unfolding bounded_def
apply clarify
@@ -2006,4 +2001,8 @@
apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
+text {* Legacy theorem names *}
+
+lemmas Lim_component_cart = tendsto_vec_nth
+
end