equal
deleted
inserted
replaced
927 also have "emeasure (Pi\<^sub>M I M) (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) = |
927 also have "emeasure (Pi\<^sub>M I M) (\<Pi>\<^sub>E j\<in>I. if j \<in> J-{i} then E j else space (M j)) = |
928 (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))" |
928 (\<Prod> j\<in>I. if j \<in> J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))" |
929 using E by (subst insert) (auto intro!: prod.cong) |
929 using E by (subst insert) (auto intro!: prod.cong) |
930 also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) * |
930 also have "(\<Prod>j\<in>I. if j \<in> J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) * |
931 emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)" |
931 emeasure (M i) (if i \<in> J then E i else space (M i)) = (\<Prod>j\<in>insert i I. ?f J E j)" |
932 using insert by (auto simp: mult.commute intro!: arg_cong2[where f="op *"] prod.cong) |
932 using insert by (auto simp: mult.commute intro!: arg_cong2[where f="( * )"] prod.cong) |
933 also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)" |
933 also have "\<dots> = (\<Prod>j\<in>J \<union> ?I. ?f J E j)" |
934 using insert(1,2) J E by (intro prod.mono_neutral_right) auto |
934 using insert(1,2) J E by (intro prod.mono_neutral_right) auto |
935 finally show "?\<mu> ?p = \<dots>" . |
935 finally show "?\<mu> ?p = \<dots>" . |
936 |
936 |
937 show "prod_emb (insert i I) M J (Pi\<^sub>E J E) \<in> Pow (\<Pi>\<^sub>E i\<in>insert i I. space (M i))" |
937 show "prod_emb (insert i I) M J (Pi\<^sub>E J E) \<in> Pow (\<Pi>\<^sub>E i\<in>insert i I. space (M i))" |