src/HOL/Analysis/Embed_Measure.thy
changeset 63886 685fb01256af
parent 63627 6ddb43c6b711
child 67241 73635a5bfa5c
     1.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Thu Sep 15 22:41:05 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Fri Sep 16 13:56:51 2016 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  lemma sets_embed_eq_vimage_algebra:
     1.5    assumes "inj_on f (space M)"
     1.6    shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)"
     1.7 -  by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 simple_image
     1.8 +  by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 Setcompr_eq_image
     1.9             dest: sets.sets_into_space
    1.10             intro!: image_cong the_inv_into_vimage[symmetric])
    1.11