src/HOL/Probability/Borel_Space.thy
changeset 44282 f0de18b62d63
parent 43923 ab93d0190a5d
child 44537 c10485a6a7af
equal deleted 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)