Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Probability/Probability_Mass_Function.thy
changeset 82802 547335b41005
parent 81995 d67dadd69d07 
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -688,7 +688,7 @@
 
 lemma pmf_map_inj': "inj f \<Longrightarrow> pmf (map_pmf f M) (f x) = pmf M x"
 apply(cases "x \<in> set_pmf M")
- apply(simp add: pmf_map_inj[OF subset_inj_on])
+ apply(simp add: pmf_map_inj[OF inj_on_subset])
 apply(simp add: pmf_eq_0_set_pmf[symmetric])
 apply(auto simp add: pmf_eq_0_set_pmf dest: injD)
 done
isabelle