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

src/HOL/Probability/Regularity.thy

changeset 60017 | b785d6d06430 |

parent 59452 | 2538b2c51769 |

child 60636 | ee18efe9b246 |

1.1 --- a/src/HOL/Probability/Regularity.thy Thu Apr 09 20:42:38 2015 +0200 1.2 +++ b/src/HOL/Probability/Regularity.thy Sat Apr 11 11:56:40 2015 +0100 1.3 @@ -363,7 +363,7 @@ 1.4 fix e::real assume "e > 0" 1.5 with measure_LIMSEQ 1.6 have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2" 1.7 - by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1) 1.8 + by (auto simp: lim_sequentially dist_real_def simp del: less_divide_eq_numeral1) 1.9 hence "\<exists>n0. \<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto 1.10 then obtain n0 where n0: "\<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2" 1.11 unfolding choice_iff by blast