equal
deleted
inserted
replaced
339 qed |
339 qed |
340 |
340 |
341 lemma Pi_pmf_return_pmf [simp]: |
341 lemma Pi_pmf_return_pmf [simp]: |
342 assumes "finite A" |
342 assumes "finite A" |
343 shows "Pi_pmf A dflt (\<lambda>x. return_pmf (f x)) = return_pmf (\<lambda>x. if x \<in> A then f x else dflt)" |
343 shows "Pi_pmf A dflt (\<lambda>x. return_pmf (f x)) = return_pmf (\<lambda>x. if x \<in> A then f x else dflt)" |
344 using assms by (intro pmf_eqI) (auto simp: pmf_Pi simp: indicator_def) |
344 using assms by (intro pmf_eqI) (auto simp: pmf_Pi simp: indicator_def split: if_splits) |
345 |
345 |
346 text \<open> |
346 text \<open> |
347 Analogously any componentwise mapping can be pulled outside the product: |
347 Analogously any componentwise mapping can be pulled outside the product: |
348 \<close> |
348 \<close> |
349 lemma Pi_pmf_map: |
349 lemma Pi_pmf_map: |