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/Projective_Limit.thy
changeset 82802 547335b41005
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Probability/Projective_Limit.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -139,7 +139,7 @@
     by unfold_locales (auto simp: Utn_def intro: from_nat_into_to_nat_on[OF countable_UN_J])
   have inj_on_Utn: "inj_on Utn (\<Union>n. J n)"
     unfolding Utn_def using countable_UN_J by (rule inj_on_to_nat_on)
-  hence inj_on_Utn_J: "\<And>n. inj_on Utn (J n)" by (rule subset_inj_on) auto
+  hence inj_on_Utn_J: "\<And>n. inj_on Utn (J n)" by (rule inj_on_subset) auto
   define P' where "P' n = mapmeasure n (P (J n)) (\<lambda>_. borel)" for n
   interpret P': prob_space "P' n" for n
     unfolding P'_def mapmeasure_def using J
isabelle