# HG changeset patch
# User hoelzl
# Date 1305627760 -7200
# Node ID b9ff5a0aa12cd98025e2e0040ae24275a8e676bb
# Parent  7d7627738e6699143f38dcabf1fdc0dee7b53a61
add restrict_sigma

diff -r 7d7627738e66 -r b9ff5a0aa12c src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue May 17 12:21:58 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue May 17 12:22:40 2011 +0200
@@ -441,6 +441,18 @@
 lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"
   unfolding sigma_def sigma_sets_eq by simp
 
+lemma restricted_sigma:
+  assumes S: "S \<in> sets (sigma M)" and M: "sets M \<subseteq> Pow (space M)"
+  shows "algebra.restricted_space (sigma M) S = sigma (algebra.restricted_space M S)"
+proof -
+  from S sigma_sets_into_sp[OF M]
+  have "S \<in> sigma_sets (space M) (sets M)" "S \<subseteq> space M"
+    by (auto simp: sigma_def)
+  from sigma_sets_Int[OF this]
+  show ?thesis
+    by (simp add: sigma_def)
+qed
+
 section {* Measurable functions *}
 
 definition