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]
```