summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Infinite_Product_Measure.thy

changeset 42866 | b0746bd57a41 |

parent 42865 | 36353d913424 |

child 42950 | 6e5c2a3c69da |

1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue May 17 12:24:48 2011 +0200 1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue May 17 14:36:54 2011 +0200 1.3 @@ -917,8 +917,9 @@ 1.4 with i show "A \<in> sigma_sets ?O ?G" 1.5 by (intro sigma_sets.Basic UN_I[where a="{i}"]) auto 1.6 qed 1.7 - finally show "sets (Pi\<^isub>P I M) = sets ?S" 1.8 + also have "\<dots> = sets ?S" 1.9 by (simp add: sets_sigma) 1.10 + finally show "sets (Pi\<^isub>P I M) = sets ?S" . 1.11 qed simp_all 1.12 1.13 lemma (in product_prob_space) measurable_into_infprod_algebra: