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