src/HOL/Analysis/Embed_Measure.thy
changeset 69566 c41954ee87cf
parent 69313 b021008c5397
child 69700 7a92cbec7030
     1.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Tue Jan 01 20:57:54 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Tue Jan 01 21:47:27 2019 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  text \<open>
     1.6    Given a measure space on some carrier set \<open>\<Omega>\<close> and a function \<open>f\<close>, we can define a push-forward
     1.7 -  measure on the carrier set $f(\Omega)$ whose \<open>\<sigma>\<close>-algebra is the one generated by mapping \<open>f\<close> over
     1.8 +  measure on the carrier set \<open>f(\<Omega>)\<close> whose \<open>\<sigma>\<close>-algebra is the one generated by mapping \<open>f\<close> over
     1.9    the original sigma algebra.
    1.10  
    1.11    This is useful e.\,g.\ when \<open>f\<close> is injective, i.\,e.\ it is some kind of ``tagging'' function.