--- 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 "\<exists>(a::'a::linorder). \<forall>x \<in> S. f x \<le> 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:"\<forall>x \<in>F. f x \<le> a" by blast
- let ?a = "max a (f x)"
- have m: "a \<le> ?a" "f x \<le> ?a" by simp_all
- {fix y assume y: "y \<in> insert x F"
- {assume "y = x" hence "f y \<le> ?a" using m by simp}
- moreover
- {assume yF: "y\<in> F" from a[rule_format, OF yF] m have "f y \<le> ?a" by (simp add: max_def)}
- ultimately have "f y \<le> ?a" using y by blast}
- then show ?case by blast
-qed
-
lemma monotone_convergence_interval: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
assumes "\<forall>k. (f k) integrable_on {a..b}"
"\<forall>k. \<forall>x\<in>{a..b}.(f k x) \<le> (f (Suc k) x)"