# HG changeset patch
# User hoelzl
# Date 1466503844 -7200
# Node ID bd37a72a940ada891eff07b3d07805886c6f1567
# Parent  158ab2239496683ae1f2088b1c94410161f6d799
Multivariate_Analysis: add continuous_on_vec_lambda

diff -r 158ab2239496 -r bd37a72a940a src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Jun 16 23:03:27 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Jun 21 12:10:44 2016 +0200
@@ -935,12 +935,16 @@
   using Basis_le_infnorm[of "axis i 1" x]
   by (simp add: Basis_vec_def axis_eq_axis inner_axis)
 
-lemma continuous_component: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x $ i)"
+lemma continuous_component[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x $ i)"
   unfolding continuous_def by (rule tendsto_vec_nth)
 
-lemma continuous_on_component: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $ i)"
+lemma continuous_on_component[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $ i)"
   unfolding continuous_on_def by (fast intro: tendsto_vec_nth)
 
+lemma continuous_on_vec_lambda[continuous_intros]:
+  "(\<And>i. continuous_on S (f i)) \<Longrightarrow> continuous_on S (\<lambda>x. \<chi> i. f i x)"
+  unfolding continuous_on_def by (auto intro: tendsto_vec_lambda)
+
 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 continuous_on_const continuous_on_id continuous_on_component)
 
@@ -1221,7 +1225,7 @@
   using assms unfolding convex_def by auto
 
 lemma convex_positive_orthant_cart: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}"
-  by (rule convex_box_cart) (simp add: atLeast_def[symmetric] convex_real_interval)
+  by (rule convex_box_cart) (simp add: atLeast_def[symmetric])
 
 lemma unit_interval_convex_hull_cart:
   "cbox (0::real^'n) 1 = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}"