author nipkow Wed, 16 Jan 2019 16:18:53 +0100 changeset 69668 14a8cac10eac parent 69667 82bb6225588b child 69669 de2f0a24b0f0
redundant lemma
```--- 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 @@
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"

-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
```--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Jan 16 15:53:12 2019 +0100