equal
deleted
inserted
replaced
393 apply (simp add: sets_PiM_single) |
393 apply (simp add: sets_PiM_single) |
394 apply (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"]) |
394 apply (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"]) |
395 apply auto [] |
395 apply auto [] |
396 apply auto [] |
396 apply auto [] |
397 apply simp |
397 apply simp |
398 apply (subst SUP_cong[OF refl]) |
398 apply (subst arg_cong [of _ _ Sup, OF image_cong, OF refl]) |
399 apply (rule sets_vimage_algebra2) |
399 apply (rule sets_vimage_algebra2) |
400 apply auto [] |
|
401 apply (auto intro!: arg_cong2[where f=sigma_sets]) |
400 apply (auto intro!: arg_cong2[where f=sigma_sets]) |
402 done |
401 done |
403 |
402 |
404 lemma%unimportant (*FIX ME needs name *) |
403 lemma%unimportant (*FIX ME needs name *) |
405 shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}" |
404 shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}" |