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/Measurable.thy
changeset 63333 158ab2239496
parent 63040 eb4ddd18d635 
--- a/src/HOL/Probability/Measurable.thy	Wed Jun 15 22:19:03 2016 +0200
+++ b/src/HOL/Probability/Measurable.thy	Thu Jun 16 23:03:27 2016 +0200
@@ -266,7 +266,7 @@
   unfolding finite_nat_set_iff_bounded by (simp add: Ball_def)
 
 lemma measurable_Least[measurable]:
-  assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"q
+  assumes [measurable]: "(\<And>i::nat. (\<lambda>x. P i x) \<in> measurable M (count_space UNIV))"
   shows "(\<lambda>x. LEAST i. P i x) \<in> measurable M (count_space UNIV)"
   unfolding measurable_def by (safe intro!: sets_Least) simp_all
isabelle