# HG changeset patch # User hoelzl # Date 1349863957 -7200 # Node ID ace9b5a83e603e1d564b8f769301ce8ceb6746ee # Parent 2f076e377703f6e8e6ac91a52cf5f76dca611259 infprod generator works also with empty index set diff -r 2f076e377703 -r ace9b5a83e60 src/HOL/Probability/Infinite_Product_Measure.thy --- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Oct 10 12:12:36 2012 +0200 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Oct 10 12:12:37 2012 +0200 @@ -174,15 +174,24 @@ qed lemma (in product_prob_space) sets_PiM_generator: - assumes "I \ {}" shows "sets (PiM I M) = sigma_sets (\\<^isub>E i\I. space (M i)) generator" -proof - show "sets (Pi\<^isub>M I M) \ sigma_sets (\\<^isub>E i\I. space (M i)) generator" - unfolding sets_PiM - proof (safe intro!: sigma_sets_subseteq) - fix A assume "A \ prod_algebra I M" with `I \ {}` show "A \ generator" - by (auto intro!: generatorI' elim!: prod_algebraE) - qed -qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset) + "sets (PiM I M) = sigma_sets (\\<^isub>E i\I. space (M i)) generator" +proof cases + assume "I = {}" then show ?thesis + unfolding generator_def + by (auto simp: sets_PiM_empty sigma_sets_empty_eq cong: conj_cong) +next + assume "I \ {}" + show ?thesis + proof + show "sets (Pi\<^isub>M I M) \ sigma_sets (\\<^isub>E i\I. space (M i)) generator" + unfolding sets_PiM + proof (safe intro!: sigma_sets_subseteq) + fix A assume "A \ prod_algebra I M" with `I \ {}` show "A \ generator" + by (auto intro!: generatorI' elim!: prod_algebraE) + qed + qed (auto simp: generator_def space_PiM[symmetric] intro!: sigma_sets_subset) +qed + lemma (in product_prob_space) generatorI: "J \ {} \ finite J \ J \ I \ X \ sets (Pi\<^isub>M J M) \ A = emb I J X \ A \ generator" @@ -628,7 +637,7 @@ using X by (auto simp add: emeasure_PiM) next show "positive (sets (Pi\<^isub>M I M)) \" "countably_additive (sets (Pi\<^isub>M I M)) \" - using \ unfolding sets_PiM_generator[OF `I \ {}`] by (auto simp: measure_space_def) + using \ unfolding sets_PiM_generator by (auto simp: measure_space_def) qed qed