author | nipkow |
Thu, 21 Dec 2017 21:38:23 +0100 | |
changeset 67241 | 73635a5bfa5c |
parent 67240 | 2c9694a8c000 |
child 67242 | a6d8458b48c0 |
--- a/src/HOL/Analysis/Embed_Measure.thy Thu Dec 21 21:01:47 2017 +0100 +++ b/src/HOL/Analysis/Embed_Measure.thy Thu Dec 21 21:38:23 2017 +0100 @@ -189,7 +189,7 @@ by(rule embed_measure_count_space')(erule subset_inj_on, simp) lemma sets_embed_measure_alt: - "inj f \<Longrightarrow> sets (embed_measure M f) = (op`f) ` sets M" + "inj f \<Longrightarrow> sets (embed_measure M f) = (op` f) ` sets M" by (auto simp: sets_embed_measure) lemma emeasure_embed_measure_image':