# HG changeset patch
# User hoelzl
# Date 1305627778 -7200
# Node ID 403e1cba11232fb8413ea826fe0d40840b0d274d
# Parent  b9ff5a0aa12cd98025e2e0040ae24275a8e676bb
add measurable_Least

diff -r b9ff5a0aa12c -r 403e1cba1123 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Tue May 17 12:22:40 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue May 17 12:22:58 2011 +0200
@@ -1429,4 +1429,37 @@
   using sigma_algebra.measurable_subset[OF sigma_algebra_sigma[OF M], of N]
   using measurable_up_sigma[of M N] N by auto
 
+lemma (in sigma_algebra) measurable_Least:
+  assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> sets M"
+  shows "(\<lambda>x. LEAST j. P j x) -` A \<inter> space M \<in> sets M"
+proof -
+  { fix i have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M \<in> sets M"
+    proof cases
+      assume i: "(LEAST j. False) = i"
+      have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
+        {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x})) \<union> (space M - (\<Union>i. {x\<in>space M. P i x}))"
+        by (simp add: set_eq_iff, safe)
+           (insert i, auto dest: Least_le intro: LeastI intro!: Least_equality)
+      with meas show ?thesis
+        by (auto intro!: Int)
+    next
+      assume i: "(LEAST j. False) \<noteq> i"
+      then have "(\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M =
+        {x\<in>space M. P i x} \<inter> (space M - (\<Union>j<i. {x\<in>space M. P j x}))"
+      proof (simp add: set_eq_iff, safe)
+        fix x assume neq: "(LEAST j. False) \<noteq> (LEAST j. P j x)"
+        have "\<exists>j. P j x"
+          by (rule ccontr) (insert neq, auto)
+        then show "P (LEAST j. P j x) x" by (rule LeastI_ex)
+      qed (auto dest: Least_le intro!: Least_equality)
+      with meas show ?thesis
+        by (auto intro!: Int)
+    qed }
+  then have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) \<in> sets M"
+    by (intro countable_UN) auto
+  moreover have "(\<Union>i\<in>A. (\<lambda>x. LEAST j. P j x) -` {i} \<inter> space M) =
+    (\<lambda>x. LEAST j. P j x) -` A \<inter> space M" by auto
+  ultimately show ?thesis by auto
+qed
+
 end