src/HOL/Probability/Borel_Space.thy
changeset 42950 6e5c2a3c69da
parent 42862 7d7627738e66
child 42990 3706951a6421
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Mon May 23 10:58:21 2011 +0200
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon May 23 19:21:05 2011 +0200
     1.3 @@ -1346,15 +1346,6 @@
     1.4      by induct auto
     1.5  qed (simp add: borel_measurable_const)
     1.6  
     1.7 -lemma abs_extreal_ge0[simp]: "0 \<le> x \<Longrightarrow> \<bar>x :: extreal\<bar> = x"
     1.8 -  by (cases x) auto
     1.9 -
    1.10 -lemma abs_extreal_less0[simp]: "x < 0 \<Longrightarrow> \<bar>x :: extreal\<bar> = -x"
    1.11 -  by (cases x) auto
    1.12 -
    1.13 -lemma abs_extreal_pos[simp]: "0 \<le> \<bar>x :: extreal\<bar>"
    1.14 -  by (cases x) auto
    1.15 -
    1.16  lemma (in sigma_algebra) borel_measurable_extreal_abs[intro, simp]:
    1.17    fixes f :: "'a \<Rightarrow> extreal" assumes "f \<in> borel_measurable M"
    1.18    shows "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"