equal
deleted
inserted
replaced
191 |
191 |
192 lemma PiM_cong: |
192 lemma PiM_cong: |
193 assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x" |
193 assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x" |
194 shows "PiM I M = PiM J N" |
194 shows "PiM I M = PiM J N" |
195 unfolding PiM_def |
195 unfolding PiM_def |
196 proof (rule extend_measure_cong, goals) |
196 proof (rule extend_measure_cong, goal_cases) |
197 case 1 |
197 case 1 |
198 show ?case using assms |
198 show ?case using assms |
199 by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all |
199 by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all |
200 next |
200 next |
201 case 2 |
201 case 2 |