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/Weak_Convergence.thy
changeset 69260 0a9688695a1b
parent 63952 354808e9f44b
child 69710 61372780515b 
--- a/src/HOL/Probability/Weak_Convergence.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Weak_Convergence.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -53,7 +53,7 @@
     by (auto intro!: cInf_lower bdd)
 
   { assume *: "I \<omega> \<le> x"
-    have "\<omega> \<le> (INF s:{x. \<omega> \<le> f x}. f s)"
+    have "\<omega> \<le> (INF s\<in>{x. \<omega> \<le> f x}. f s)"
       by (rule cINF_greatest[OF ne]) auto
     also have "\<dots> = f (I \<omega>)"
       using continuous_at_Inf_mono[OF mono cont ne bdd] ..
isabelle