summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Finite_Product_Measure.thy

changeset 57025 | e7fd64f82876 |

parent 56996 | 891e992e510f |

child 57418 | 6ab1c7cb0b8d |

1.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy Tue May 20 16:52:59 2014 +0200 1.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue May 20 19:24:39 2014 +0200 1.3 @@ -497,6 +497,10 @@ 1.4 using A X by (auto intro!: measurable_sets) 1.5 qed (insert X, auto simp add: PiE_def dest: measurable_space) 1.6 1.7 +lemma measurable_abs_UNIV: 1.8 + "(\<And>n. (\<lambda>\<omega>. f n \<omega>) \<in> measurable M (N n)) \<Longrightarrow> (\<lambda>\<omega> n. f n \<omega>) \<in> measurable M (PiM UNIV N)" 1.9 + by (intro measurable_PiM_single) (auto dest: measurable_space) 1.10 + 1.11 lemma measurable_restrict_subset: "J \<subseteq> L \<Longrightarrow> (\<lambda>f. restrict f J) \<in> measurable (Pi\<^sub>M L M) (Pi\<^sub>M J M)" 1.12 by (intro measurable_restrict measurable_component_singleton) auto 1.13