# HG changeset patch
# User hoelzl
# Date 1427102180 -3600
# Node ID fe5b796d6b2a9e5be9546bc28a794fb230a735e0
# Parent  9ad96e97e72daa41949f6dc15c2859844359fdde
add measurable_submarkov

diff -r 9ad96e97e72d -r fe5b796d6b2a src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Mon Mar 23 08:45:54 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Mon Mar 23 10:16:20 2015 +0100
@@ -221,6 +221,22 @@
   K \<in> measurable M (subprob_algebra N)"
   by (auto intro!: measurable_Sup_sigma2 measurable_vimage_algebra2 simp: subprob_algebra_def)
 
+lemma measurable_submarkov:
+  "K \<in> measurable M (subprob_algebra M) \<longleftrightarrow>
+    (\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
+    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> measurable M borel)"
+proof
+  assume "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
+    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"
+  then show "K \<in> measurable M (subprob_algebra M)"
+    by (intro measurable_subprob_algebra) auto
+next
+  assume "K \<in> measurable M (subprob_algebra M)"
+  then show "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
+    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"
+    by (auto dest: subprob_space_kernel sets_kernel)
+qed
+
 lemma space_subprob_algebra_empty_iff:
   "space (subprob_algebra N) = {} \<longleftrightarrow> space N = {}"
 proof