# HG changeset patch # User hoelzl # Date 1299146141 -3600 # Node ID a3035d56171d0677b8f3ab7754bf141a97e969e5 # Parent 250468a1bd7a9fa49f946a515c6682fb8c4a8812 finally remove upper_bound_finite_set diff -r 250468a1bd7a -r a3035d56171d src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Mar 03 15:59:44 2011 +1100 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Mar 03 10:55:41 2011 +0100 @@ -4470,24 +4470,6 @@ subsection {* monotone convergence (bounded interval first). *} -lemma upper_bound_finite_set: - assumes fS: "finite S" - shows "\(a::'a::linorder). \x \ S. f x \ a" -proof(induct rule: finite_induct[OF fS]) - case 1 thus ?case by simp -next - case (2 x F) - from "2.hyps" obtain a where a:"\x \F. f x \ a" by blast - let ?a = "max a (f x)" - have m: "a \ ?a" "f x \ ?a" by simp_all - {fix y assume y: "y \ insert x F" - {assume "y = x" hence "f y \ ?a" using m by simp} - moreover - {assume yF: "y\ F" from a[rule_format, OF yF] m have "f y \ ?a" by (simp add: max_def)} - ultimately have "f y \ ?a" using y by blast} - then show ?case by blast -qed - lemma monotone_convergence_interval: fixes f::"nat \ 'n::ordered_euclidean_space \ real" assumes "\k. (f k) integrable_on {a..b}" "\k. \x\{a..b}.(f k x) \ (f (Suc k) x)"