# HG changeset patch
# User nipkow
# Date 1547651933 -3600
# Node ID 14a8cac10eac7d220bcee68b185b298cec61741f
# Parent  82bb6225588ba603cfc698432fb1fc4256cef194
redundant lemma

diff -r 82bb6225588b -r 14a8cac10eac src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Jan 16 15:53:12 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Jan 16 16:18:53 2019 +0100
@@ -952,10 +952,6 @@
   apply (simp add: forall_3)
   done
 
-lemma bounded_linear_component_cart[intro]: "bounded_linear (\<lambda>x::real^'n. x $ k)"
-  apply (rule bounded_linear_intro[where K=1])
-  using component_le_norm_cart[of _ k] unfolding real_norm_def by auto
-
 lemma interval_split_cart:
   "{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
   "cbox a b \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}"
@@ -967,6 +963,5 @@
 lemmas cartesian_euclidean_space_uniform_limit_intros[uniform_limit_intros] =
   bounded_linear.uniform_limit[OF blinfun.bounded_linear_right]
   bounded_linear.uniform_limit[OF bounded_linear_vec_nth]
-  bounded_linear.uniform_limit[OF bounded_linear_component_cart]
 
 end
diff -r 82bb6225588b -r 14a8cac10eac src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Jan 16 15:53:12 2019 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Wed Jan 16 16:18:53 2019 +0100
@@ -626,7 +626,7 @@
 lemma%unimportant norm_le_l1_cart: "norm x \<le> sum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
   by (simp add: norm_vec_def L2_set_le_sum)
 
-lemma%unimportant bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)"
+lemma%unimportant bounded_linear_vec_nth[intro]: "bounded_linear (\<lambda>x. x $ i)"
 apply standard
 apply (rule vector_add_component)
 apply (rule vector_scaleR_component)
diff -r 82bb6225588b -r 14a8cac10eac src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Jan 16 15:53:12 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Jan 16 16:18:53 2019 +0100
@@ -7489,7 +7489,7 @@
   fixes f :: "'n::euclidean_space \<Rightarrow> real^'m"
   assumes "f integrable_on s"
   shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
-  using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] .
+  using integral_linear[OF assms(1) bounded_linear_vec_nth,unfolded o_def] .
 
 lemma content_closed_interval:
   fixes a :: "'a::ordered_euclidean_space"