src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
 changeset 63938 f6ce08859d4c parent 63928 d81fb5b46a5c child 63940 0d82c4c94014
```     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Sep 21 16:59:51 2016 +0100
1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 22 15:44:47 2016 +0100
1.3 @@ -2902,7 +2902,7 @@
1.4    fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
1.5    assumes "f integrable_on s"
1.6    shows "integral s (\<lambda>x. f x \<bullet> k) = integral s f \<bullet> k"
1.7 -  unfolding integral_linear[OF assms(1) bounded_linear_component,unfolded o_def] ..
1.8 +  unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] ..
1.9
1.10  lemma has_integral_setsum:
1.11    assumes "finite t"
1.12 @@ -3090,7 +3090,7 @@
1.13    shows "(f has_integral y) A \<longleftrightarrow> (\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
1.14  proof safe
1.15    fix b :: 'b assume "(f has_integral y) A"
1.16 -  from has_integral_linear[OF this(1) bounded_linear_component, of b]
1.17 +  from has_integral_linear[OF this(1) bounded_linear_inner_left, of b]
1.18      show "((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A" by (simp add: o_def)
1.19  next
1.20    assume "(\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
1.21 @@ -3148,7 +3148,7 @@
1.22
1.23  lemma integrable_component:
1.24    "f integrable_on A \<Longrightarrow> (\<lambda>x. f x \<bullet> (y :: 'b :: euclidean_space)) integrable_on A"
1.25 -  by (drule integrable_linear[OF _ bounded_linear_component[of y]]) (simp add: o_def)
1.26 +  by (drule integrable_linear[OF _ bounded_linear_inner_left[of y]]) (simp add: o_def)
1.27
1.28
1.29
```