Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Probability/Borel_Space.thy
changeset 53216 ad2e09c30aa8
parent 51683 baefa3b461c2
child 54230 b1d955791529 
--- a/src/HOL/Probability/Borel_Space.thy	Tue Aug 27 14:37:56 2013 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Aug 27 16:06:27 2013 +0200
@@ -251,7 +251,7 @@
   by (blast intro: borel_open borel_closed)+
 
 lemma open_Collect_less:
-  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
   assumes "continuous_on UNIV f"
   assumes "continuous_on UNIV g"
   shows "open {x. f x < g x}"
@@ -264,14 +264,14 @@
 qed
 
 lemma closed_Collect_le:
-  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {dense_linorder, linorder_topology}"
   assumes f: "continuous_on UNIV f"
   assumes g: "continuous_on UNIV g"
   shows "closed {x. f x \<le> g x}"
   using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
 
 lemma borel_measurable_less[measurable]:
-  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows "{w \<in> space M. f w < g w} \<in> sets M"
@@ -285,7 +285,7 @@
 qed
 
 lemma
-  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology}"
   assumes f[measurable]: "f \<in> borel_measurable M"
   assumes g[measurable]: "g \<in> borel_measurable M"
   shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
@@ -755,11 +755,11 @@
   by (simp add: field_divide_inverse)
 
 lemma borel_measurable_max[measurable (raw)]:
-  "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"
+  "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"
   by (simp add: max_def)
 
 lemma borel_measurable_min[measurable (raw)]:
-  "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"
+  "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"
   by (simp add: min_def)
 
 lemma borel_measurable_abs[measurable (raw)]:
isabelle