summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Probability/Conditional_Expectation.thy

changeset 70125 | b601c2c87076 |

parent 69712 | dc85b5b3a532 |

child 70817 | dd675800469d |

1.1 --- a/src/HOL/Probability/Conditional_Expectation.thy Wed Apr 10 23:12:27 2019 +0100 1.2 +++ b/src/HOL/Probability/Conditional_Expectation.thy Thu Apr 11 15:26:04 2019 +0100 1.3 @@ -994,7 +994,7 @@ 1.4 moreover have "real_cond_exp M F f x \<ge> c" if "\<forall>n. real_cond_exp M F f x > u n" for x 1.5 proof - 1.6 have "real_cond_exp M F f x \<ge> u n" for n using that less_imp_le by auto 1.7 - then show ?thesis using u(2) LIMSEQ_le_const2 by blast 1.8 + then show ?thesis using u(2) LIMSEQ_le_const2 by metis 1.9 qed 1.10 ultimately show ?thesis by auto 1.11 qed