# HG changeset patch
# User immler
# Date 1460549571 -7200
# Node ID 2d5eff9c3baae5ac8819682961e8c5067e1c3d76
# Parent  1c1f8531ca372e8efd14d6b188004bbe35e6e48d
added rule

diff -r 1c1f8531ca37 -r 2d5eff9c3baa src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Tue Apr 12 18:49:39 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Wed Apr 13 14:12:51 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