summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Probability/Fin_Map.thy

changeset 50100 | 9af8721ecd20 |

parent 50094 | 84ddcf5364b4 |

child 50123 | 69b35a75caf3 |

--- a/src/HOL/Probability/Fin_Map.thy Fri Nov 16 14:46:23 2012 +0100 +++ b/src/HOL/Probability/Fin_Map.thy Fri Nov 16 14:46:23 2012 +0100 @@ -1278,7 +1278,7 @@ subsection {* Isomorphism between Functions and Finite Maps *} lemma - measurable_compose: + measurable_finmap_compose: fixes f::"'a \<Rightarrow> 'b" assumes inj: "\<And>j. j \<in> J \<Longrightarrow> f' (f j) = j" assumes "finite J" @@ -1326,7 +1326,7 @@ shows "(\<lambda>m. compose (f ` J) m f') \<in> measurable (PiM J (\<lambda>_. M)) (PiM (f ` J) (\<lambda>_. M))" proof - have "(\<lambda>m. compose (f ` J) m f') \<in> measurable (Pi\<^isub>M (f' ` f ` J) (\<lambda>_. M)) (Pi\<^isub>M (f ` J) (\<lambda>_. M))" - using assms by (auto intro: measurable_compose) + using assms by (auto intro: measurable_finmap_compose) moreover from inj have "f' ` f ` J = J" by (metis (hide_lams, mono_tags) image_iff set_eqI) ultimately show ?thesis by simp @@ -1426,7 +1426,7 @@ proof (rule measurable_comp, rule measurable_proj_PiM) show "(\<lambda>g. compose J g f) \<in> measurable (Pi\<^isub>M (f ` J) (\<lambda>x. M)) (Pi\<^isub>M J (\<lambda>_. M))" - by (rule measurable_compose, rule inv) auto + by (rule measurable_finmap_compose, rule inv) auto qed (auto simp add: space_PiM extensional_def assms) lemma fm_image_measurable: