src/HOL/Analysis/Convex_Euclidean_Space.thy
changeset 69510 0f31dd2e540d
parent 69508 2a4c8a2a3f8e
child 69518 bf88364c9e94
     1.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Dec 27 19:48:41 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Dec 27 21:00:50 2018 +0100
     1.3 @@ -2637,9 +2637,9 @@
     1.4      }
     1.5      moreover
     1.6      have "(\<Sum>v\<in>y ` {1..k}. sum u {i \<in> {1..k}. y i = v}) = 1"
     1.7 -      unfolding sum_image_gen[OF fin, symmetric] using obt(2) by auto
     1.8 +      unfolding sum.image_gen[OF fin, symmetric] using obt(2) by auto
     1.9      moreover have "(\<Sum>v\<in>y ` {1..k}. sum u {i \<in> {1..k}. y i = v} *\<^sub>R v) = x"
    1.10 -      using sum_image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, symmetric]
    1.11 +      using sum.image_gen[OF fin, of "\<lambda>i. u i *\<^sub>R y i" y, symmetric]
    1.12        unfolding scaleR_left.sum using obt(3) by auto
    1.13      ultimately
    1.14      have "\<exists>S u. finite S \<and> S \<subseteq> p \<and> (\<forall>x\<in>S. 0 \<le> u x) \<and> sum u S = 1 \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = x"
    1.15 @@ -2683,8 +2683,8 @@
    1.16          by (auto simp: sum_constant_scaleR)
    1.17      }
    1.18      then have "(\<Sum>x = 1..card S. u (f x)) = 1" "(\<Sum>i = 1..card S. u (f i) *\<^sub>R f i) = y"
    1.19 -      unfolding sum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f]
    1.20 -        and sum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
    1.21 +      unfolding sum.image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f]
    1.22 +        and sum.image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
    1.23        unfolding f
    1.24        using sum.cong [of S S "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card S}. f x = y}. u (f x) *\<^sub>R f x)" "\<lambda>v. u v *\<^sub>R v"]
    1.25        using sum.cong [of S S "\<lambda>y. (\<Sum>x\<in>{x \<in> {1..card S}. f x = y}. u (f x))" u]