equal
deleted
inserted
replaced
527 done |
527 done |
528 |
528 |
529 lemma Blinfun_eq_matrix: "bounded_linear f \<Longrightarrow> Blinfun f = blinfun_of_matrix (\<lambda>i j. f j \<bullet> i)" |
529 lemma Blinfun_eq_matrix: "bounded_linear f \<Longrightarrow> Blinfun f = blinfun_of_matrix (\<lambda>i j. f j \<bullet> i)" |
530 by (intro blinfun_euclidean_eqI) |
530 by (intro blinfun_euclidean_eqI) |
531 (auto simp: blinfun_of_matrix_apply bounded_linear_Blinfun_apply inner_Basis if_distrib |
531 (auto simp: blinfun_of_matrix_apply bounded_linear_Blinfun_apply inner_Basis if_distrib |
532 cond_application_beta sum.delta' euclidean_representation |
532 if_distribR sum.delta' euclidean_representation |
533 cong: if_cong) |
533 cong: if_cong) |
534 |
534 |
535 text \<open>TODO: generalize (via \<open>compact_cball\<close>)?\<close> |
535 text \<open>TODO: generalize (via \<open>compact_cball\<close>)?\<close> |
536 instance blinfun :: (euclidean_space, euclidean_space) heine_borel |
536 instance blinfun :: (euclidean_space, euclidean_space) heine_borel |
537 proof |
537 proof |