# 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 "\i j. i \ Basis \ j \ Basis \ continuous_on S (\s. g s i j)" + shows "continuous_on S (\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