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