213 |
213 |
214 interpretation blinfun: bounded_bilinear blinfun_apply |
214 interpretation blinfun: bounded_bilinear blinfun_apply |
215 by (rule bounded_bilinear_blinfun_apply) |
215 by (rule bounded_bilinear_blinfun_apply) |
216 |
216 |
217 lemmas bounded_linear_apply_blinfun[intro, simp] = blinfun.bounded_linear_left |
217 lemmas bounded_linear_apply_blinfun[intro, simp] = blinfun.bounded_linear_left |
|
218 |
|
219 declare blinfun.zero_left [simp] blinfun.zero_right [simp] |
218 |
220 |
219 |
221 |
220 context bounded_bilinear |
222 context bounded_bilinear |
221 begin |
223 begin |
222 |
224 |
680 lemma blinfun_compose_zero[simp]: |
682 lemma blinfun_compose_zero[simp]: |
681 "blinfun_compose 0 = (\<lambda>_. 0)" |
683 "blinfun_compose 0 = (\<lambda>_. 0)" |
682 "blinfun_compose x 0 = 0" |
684 "blinfun_compose x 0 = 0" |
683 by (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI) |
685 by (auto simp: blinfun.bilinear_simps intro!: blinfun_eqI) |
684 |
686 |
|
687 lemma blinfun_bij2: |
|
688 fixes f::"'a \<Rightarrow>\<^sub>L 'a::euclidean_space" |
|
689 assumes "f o\<^sub>L g = id_blinfun" |
|
690 shows "bij (blinfun_apply g)" |
|
691 proof (rule bijI) |
|
692 show "inj g" |
|
693 using assms |
|
694 by (metis blinfun_apply_id_blinfun blinfun_compose.rep_eq injI inj_on_imageI2) |
|
695 then show "surj g" |
|
696 using blinfun.bounded_linear_right bounded_linear_def linear_inj_imp_surj by blast |
|
697 qed |
|
698 |
|
699 lemma blinfun_bij1: |
|
700 fixes f::"'a \<Rightarrow>\<^sub>L 'a::euclidean_space" |
|
701 assumes "f o\<^sub>L g = id_blinfun" |
|
702 shows "bij (blinfun_apply f)" |
|
703 proof (rule bijI) |
|
704 show "surj (blinfun_apply f)" |
|
705 by (metis assms blinfun_apply_blinfun_compose blinfun_apply_id_blinfun surjI) |
|
706 then show "inj (blinfun_apply f)" |
|
707 using blinfun.bounded_linear_right bounded_linear_def linear_surj_imp_inj by blast |
|
708 qed |
685 |
709 |
686 lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "(\<bullet>)" |
710 lift_definition blinfun_inner_right::"'a::real_inner \<Rightarrow> 'a \<Rightarrow>\<^sub>L real" is "(\<bullet>)" |
687 by (rule bounded_linear_inner_right) |
711 by (rule bounded_linear_inner_right) |
688 declare blinfun_inner_right.rep_eq[simp] |
712 declare blinfun_inner_right.rep_eq[simp] |
689 |
713 |