src/HOL/Probability/Borel_Space.thy
changeset 53216 ad2e09c30aa8
parent 51683 baefa3b461c2
child 54230 b1d955791529
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Aug 27 14:37:56 2013 +0200
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Aug 27 16:06:27 2013 +0200
     1.3 @@ -251,7 +251,7 @@
     1.4    by (blast intro: borel_open borel_closed)+
     1.5  
     1.6  lemma open_Collect_less:
     1.7 -  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
     1.8 +  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
     1.9    assumes "continuous_on UNIV f"
    1.10    assumes "continuous_on UNIV g"
    1.11    shows "open {x. f x < g x}"
    1.12 @@ -264,14 +264,14 @@
    1.13  qed
    1.14  
    1.15  lemma closed_Collect_le:
    1.16 -  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
    1.17 +  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
    1.18    assumes f: "continuous_on UNIV f"
    1.19    assumes g: "continuous_on UNIV g"
    1.20    shows "closed {x. f x \<le> g x}"
    1.21    using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
    1.22  
    1.23  lemma borel_measurable_less[measurable]:
    1.24 -  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
    1.25 +  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
    1.26    assumes "f \<in> borel_measurable M"
    1.27    assumes "g \<in> borel_measurable M"
    1.28    shows "{w \<in> space M. f w < g w} \<in> sets M"
    1.29 @@ -285,7 +285,7 @@
    1.30  qed
    1.31  
    1.32  lemma
    1.33 -  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
    1.34 +  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
    1.35    assumes f[measurable]: "f \<in> borel_measurable M"
    1.36    assumes g[measurable]: "g \<in> borel_measurable M"
    1.37    shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
    1.38 @@ -755,11 +755,11 @@
    1.39    by (simp add: field_divide_inverse)
    1.40  
    1.41  lemma borel_measurable_max[measurable (raw)]:
    1.42 -  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
    1.43 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
    1.44    by (simp add: max_def)
    1.45  
    1.46  lemma borel_measurable_min[measurable (raw)]:
    1.47 -  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
    1.48 +  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, dense_linorder, linorder_topology}) \<in> borel_measurable M"
    1.49    by (simp add: min_def)
    1.50  
    1.51  lemma borel_measurable_abs[measurable (raw)]: