--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Dec 01 20:12:53 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Dec 01 21:03:02 2010 +0100
@@ -403,6 +403,12 @@
shows "sets (sigma N) \<subseteq> sets M"
by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms)
+lemma in_sigma[intro, simp]: "A \<in> sets M \<Longrightarrow> A \<in> sets (sigma M)"
+ unfolding sigma_def by (auto intro!: sigma_sets.Basic)
+
+lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M"
+ unfolding sigma_def sigma_sets_eq by simp
+
section {* Measurable functions *}
definition
@@ -865,6 +871,22 @@
qed
qed
+lemma vimage_algebra_sigma:
+ assumes E: "sets E \<subseteq> Pow (space E)"
+ and f: "f \<in> space F \<rightarrow> space E"
+ and "\<And>A. A \<in> sets F \<Longrightarrow> A \<in> (\<lambda>X. f -` X \<inter> space F) ` sets E"
+ and "\<And>A. A \<in> sets E \<Longrightarrow> f -` A \<inter> space F \<in> sets F"
+ shows "sigma_algebra.vimage_algebra (sigma E) (space F) f = sigma F"
+proof -
+ interpret sigma_algebra "sigma E"
+ using assms by (intro sigma_algebra_sigma) auto
+ have eq: "sets F = (\<lambda>X. f -` X \<inter> space F) ` sets E"
+ using assms by auto
+ show "vimage_algebra (space F) f = sigma F"
+ unfolding vimage_algebra_def using assms
+ by (simp add: sigma_def eq sigma_sets_vimage)
+qed
+
section {* Conditional space *}
definition (in algebra)