
diff -r d31e986fbebc -r f8b98d31ad45 src/HOL/Probability/Distribution_Functions.thy
--- a/src/HOL/Probability/Distribution_Functions.thy	Thu Jun 28 14:14:05 2018 +0100
+++ b/src/HOL/Probability/Distribution_Functions.thy	Thu Jun 28 17:14:40 2018 +0100
@@ -107,7 +107,7 @@
     using \<open>decseq f\<close> unfolding cdf_def
     by (intro finite_Lim_measure_decseq) (auto simp: decseq_def)
   also have "(\<Inter>i. {.. f i}) = {.. a}"
-    using decseq_le[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
+    using decseq_ge[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
   finally show "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> cdf M a"
     by (simp add: cdf_def)
 qed simp




