finally remove upper_bound_finite_set
authorhoelzl
Thu Mar 03 10:55:41 2011 +0100 (2011-03-03)
changeset 41874a3035d56171d
parent 41873 250468a1bd7a
child 41875 e3cd0dce9b1a
child 41879 7f9c48c17d2a
finally remove upper_bound_finite_set
src/HOL/Multivariate_Analysis/Integration.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Mar 03 15:59:44 2011 +1100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Thu Mar 03 10:55:41 2011 +0100
     1.3 @@ -4470,24 +4470,6 @@
     1.4  
     1.5  subsection {* monotone convergence (bounded interval first). *}
     1.6  
     1.7 -lemma upper_bound_finite_set:
     1.8 -  assumes fS: "finite S"
     1.9 -  shows "\<exists>(a::'a::linorder). \<forall>x \<in> S. f x \<le> a"
    1.10 -proof(induct rule: finite_induct[OF fS])
    1.11 -  case 1 thus ?case by simp
    1.12 -next
    1.13 -  case (2 x F)
    1.14 -  from "2.hyps" obtain a where a:"\<forall>x \<in>F. f x \<le> a" by blast
    1.15 -  let ?a = "max a (f x)"
    1.16 -  have m: "a \<le> ?a" "f x \<le> ?a" by simp_all
    1.17 -  {fix y assume y: "y \<in> insert x F"
    1.18 -    {assume "y = x" hence "f y \<le> ?a" using m by simp}
    1.19 -    moreover
    1.20 -    {assume yF: "y\<in> F" from a[rule_format, OF yF] m have "f y \<le> ?a" by (simp add: max_def)}
    1.21 -    ultimately have "f y \<le> ?a" using y by blast}
    1.22 -  then show ?case by blast
    1.23 -qed
    1.24 -
    1.25  lemma monotone_convergence_interval: fixes f::"nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
    1.26    assumes "\<forall>k. (f k) integrable_on {a..b}"
    1.27    "\<forall>k. \<forall>x\<in>{a..b}.(f k x) \<le> (f (Suc k) x)"