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

src/HOL/Probability/Infinite_Product_Measure.thy

changeset 46898 | 1570b30ee040 |

parent 46731 | 5302e932d1e5 |

child 46905 | 6b1c0a80a57a |

1.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy Tue Mar 13 12:51:52 2012 +0100 1.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Tue Mar 13 13:31:26 2012 +0100 1.3 @@ -502,7 +502,7 @@ 1.4 fix A assume "A \<in> sets ?G" 1.5 with generatorE guess J X . note JX = this 1.6 interpret JK: finite_product_prob_space M J by default fact+ 1.7 - with JX show "\<mu>G A \<noteq> \<infinity>" by simp 1.8 + from JX show "\<mu>G A \<noteq> \<infinity>" by simp 1.9 next 1.10 fix A assume A: "range A \<subseteq> sets ?G" "decseq A" "(\<Inter>i. A i) = {}" 1.11 then have "decseq (\<lambda>i. \<mu>G (A i))"