| changeset 54420 | 1e6412c82837 |
| parent 54418 | 3b8e33d1a39a |
| child 56154 | f0a927235162 |
--- a/src/HOL/Probability/Sigma_Algebra.thy Tue Nov 12 20:08:29 2013 +0100 +++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Nov 13 09:37:00 2013 +0100 @@ -1756,7 +1756,7 @@ qed auto qed -subsection {* Restricted Space \<sigma>-Algebra *} +subsection {* Restricted Space Sigma Algebra *} definition "restrict_space M \<Omega> = measure_of \<Omega> ((op \<inter> \<Omega>) ` sets M) (\<lambda>A. emeasure M (A \<inter> \<Omega>))"