summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.