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/Embed_Measure.thy
changeset 82802 547335b41005
parent 71633 07bec530f02e 
--- a/src/HOL/Analysis/Embed_Measure.thy	Tue Jul 01 20:51:26 2025 +0200
+++ b/src/HOL/Analysis/Embed_Measure.thy	Thu Jul 03 13:53:14 2025 +0200
@@ -132,7 +132,7 @@
 lemma nn_integral_embed_measure:
   "inj f \<Longrightarrow> g \<in> borel_measurable (embed_measure M f) \<Longrightarrow>
   nn_integral (embed_measure M f) g = nn_integral M (\<lambda>x. g (f x))"
-  by(erule nn_integral_embed_measure'[OF subset_inj_on]) simp
+  by(erule nn_integral_embed_measure'[OF inj_on_subset]) simp
 
 lemma emeasure_embed_measure':
     assumes "inj_on f (space M)" "A \<in> sets (embed_measure M f)"
@@ -196,7 +196,7 @@
 
 lemma embed_measure_count_space:
     "inj f \<Longrightarrow> embed_measure (count_space A) f = count_space (f`A)"
-  by(rule embed_measure_count_space')(erule subset_inj_on, simp)
+  by(rule embed_measure_count_space')(erule inj_on_subset, simp)
 
 lemma sets_embed_measure_alt:
     "inj f \<Longrightarrow> sets (embed_measure M f) = ((`) f) ` sets M"
isabelle