# HG changeset patch
# User wenzelm
# Date 1460563467 -7200
# Node ID f78cf782bd33e90ebfd369986e5abf427cf4229d
# Parent  2d5eff9c3baae5ac8819682961e8c5067e1c3d76# Parent  9f394a16c557410fb2a530b06e8a9a6d4e47d08b
merged

diff -r 9f394a16c557 -r f78cf782bd33 src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Wed Apr 13 18:01:05 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Wed Apr 13 18:04:27 2016 +0200
@@ -463,6 +463,12 @@
   using assms
   by (auto simp: continuous_on_eq_continuous_within continuous_blinfun_matrix)
 
+lemma continuous_on_blinfun_of_matrix[continuous_intros]:
+  assumes "\<And>i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> continuous_on S (\<lambda>s. g s i j)"
+  shows "continuous_on S (\<lambda>s. blinfun_of_matrix (g s))"
+  using assms
+  by (auto simp: continuous_on intro!: tendsto_blinfun_of_matrix)
+
 lemma mult_if_delta:
   "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)"
   by auto