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/Essential_Supremum.thy
changeset 69260 0a9688695a1b
parent 68751 640386ab99f3 
--- a/src/HOL/Probability/Essential_Supremum.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Essential_Supremum.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -30,13 +30,13 @@
   fix y assume "AE x in M. f x \<le> y"
   then have "(\<lambda>x. f x \<le> y) \<in> {P. AE x in M. P x}"
     by simp
-  then show "(INF P:{P. AE x in M. P x}. SUP x:Collect P. f x) \<le> y"
+  then show "(INF P\<in>{P. AE x in M. P x}. SUP x\<in>Collect P. f x) \<le> y"
     by (rule INF_lower2) (auto intro: SUP_least)
 next
   fix P assume P: "AE x in M. P x"
-  show "Inf {z. AE x in M. f x \<le> z} \<le> (SUP x:Collect P. f x)"
+  show "Inf {z. AE x in M. f x \<le> z} \<le> (SUP x\<in>Collect P. f x)"
   proof (rule Inf_lower; clarsimp)
-    show "AE x in M. f x \<le> (SUP x:Collect P. f x)"
+    show "AE x in M. f x \<le> (SUP x\<in>Collect P. f x)"
       using P by (auto elim: eventually_mono simp: SUP_upper)
   qed
 qed
isabelle