# HG changeset patch
# User immler
# Date 1460452709 -7200
# Node ID f59ef58f420b71d73dd431d2b21c20e9c547e902
# Parent  c355b3223cbdda9d7cabad782139228b00db598f
added lemmas

diff -r c355b3223cbd -r f59ef58f420b src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Tue Apr 12 11:18:29 2016 +0200
@@ -484,6 +484,12 @@
   apply (simp add: blinfun.bilinear_simps)
   done
 
+lemma Blinfun_eq_matrix: "bounded_linear f \<Longrightarrow> Blinfun f = blinfun_of_matrix (\<lambda>i j. f j \<bullet> i)"
+  by (intro blinfun_euclidean_eqI)
+     (auto simp: blinfun_of_matrix_apply bounded_linear_Blinfun_apply inner_Basis if_distrib
+      cond_application_beta setsum.delta' euclidean_representation
+      cong: if_cong)
+
 text \<open>TODO: generalize (via @{thm compact_cball})?\<close>
 instance blinfun :: (euclidean_space, euclidean_space) heine_borel
 proof
@@ -627,6 +633,11 @@
   by unfold_locales
     (auto intro!: blinfun_eqI exI[where x=1] simp: blinfun.bilinear_simps norm_blinfun_compose)
 
+lemma blinfun_compose_zero[simp]:
+  "blinfun_compose 0 = (\<lambda>_. 0)"
+  "blinfun_compose x 0 = 0"
+  by (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI)
+
 
 lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "op \<bullet>"
   by (rule bounded_linear_inner_right)