--- 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
--- 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)
--- 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"