src/HOL/Probability/Borel_Space.thy
 changeset 44282 f0de18b62d63 parent 43923 ab93d0190a5d child 44537 c10485a6a7af
equal inserted replaced
44275:d995733b635d 44282:f0de18b62d63
`   814   fix S :: "'x set" assume "open S"`
`   814   fix S :: "'x set" assume "open S"`
`   815   show "(\<lambda>x. a + b *\<^sub>R f x) -` S \<inter> space M \<in> sets M"`
`   815   show "(\<lambda>x. a + b *\<^sub>R f x) -` S \<inter> space M \<in> sets M"`
`   816   proof cases`
`   816   proof cases`
`   817     assume "b \<noteq> 0"`
`   817     assume "b \<noteq> 0"`
`   818     with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")`
`   818     with `open S` have "((\<lambda>x. (- a + x) /\<^sub>R b) ` S) \<in> open" (is "?S \<in> open")`
`   819       by (auto intro!: open_affinity simp: scaleR.add_right mem_def)`
`   819       by (auto intro!: open_affinity simp: scaleR_add_right mem_def)`
`   820     hence "?S \<in> sets borel"`
`   820     hence "?S \<in> sets borel"`
`   821       unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic)`
`   821       unfolding borel_def by (auto simp: sigma_def intro!: sigma_sets.Basic)`
`   822     moreover`
`   822     moreover`
`   823     from `b \<noteq> 0` have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"`
`   823     from `b \<noteq> 0` have "(\<lambda>x. a + b *\<^sub>R f x) -` S = f -` ?S"`
`   824       apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all)`
`   824       apply auto by (rule_tac x="a + b *\<^sub>R f x" in image_eqI, simp_all)`