equal
deleted
inserted
replaced
314 "convex_bind_basis = fold_pd |
314 "convex_bind_basis = fold_pd |
315 (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a)) |
315 (\<lambda>a. \<Lambda> f. f\<cdot>(Rep_compact_basis a)) |
316 (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)" |
316 (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)" |
317 |
317 |
318 lemma ACI_convex_bind: |
318 lemma ACI_convex_bind: |
319 "class.ab_semigroup_idem_mult (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)" |
319 "semilattice (\<lambda>x y. \<Lambda> f. x\<cdot>f \<union>\<natural> y\<cdot>f)" |
320 apply unfold_locales |
320 apply unfold_locales |
321 apply (simp add: convex_plus_assoc) |
321 apply (simp add: convex_plus_assoc) |
322 apply (simp add: convex_plus_commute) |
322 apply (simp add: convex_plus_commute) |
323 apply (simp add: eta_cfun) |
323 apply (simp add: eta_cfun) |
324 done |
324 done |