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/Analysis/Measure_Space.thy
changeset 82802 547335b41005
parent 82538 4b132ea7d575 
--- a/src/HOL/Analysis/Measure_Space.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -2365,7 +2365,7 @@
   moreover have "inj_on (the_inv_into A f) B"
     using X f by (auto simp: bij_betw_def inj_on_the_inv_into)
   with X have "inj_on (the_inv_into A f) X"
-    by (auto intro: subset_inj_on)
+    by (auto intro: inj_on_subset)
   ultimately show "emeasure (distr (count_space A) (count_space B) f) X = emeasure (count_space B) X"
     using f unfolding emeasure_distr[OF f' X]
     by (subst (1 2) emeasure_count_space) (auto simp: card_image dest: finite_imageD)
isabelle