changeset 61753 865bb718bdb9 parent 61634 48e2de1b1df5 child 61808 fc1556774cfe
equal inserted replaced
61752:814bbe5d9204 61753:865bb718bdb9
`   277 next`
`   277 next`
`   278   case (mult f c)`
`   278   case (mult f c)`
`   279   moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"`
`   279   moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"`
`   280     by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)`
`   280     by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)`
`   281   ultimately show ?case`
`   281   ultimately show ?case`
`   283     by simp`
`   282     by simp`
`   284 next`
`   283 next`
`   285   case (add f g)`
`   284   case (add f g)`
`   286   moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"`
`   285   moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"`
`   287     by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)`
`   286     by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)`