src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
changeset 51478 270b21f3ae0a
parent 50884 2b21b4e2d7cb
child 53185 752e05d09708
     1.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -26,14 +26,6 @@
     1.4  lemma divide_nonneg_nonneg:assumes "a \<ge> 0" "b \<ge> 0" shows "0 \<le> a / (b::real)"
     1.5    apply(cases "b=0") defer apply(rule divide_nonneg_pos) using assms by auto
     1.6  
     1.7 -lemma continuous_setsum:
     1.8 -  fixes f :: "'i \<Rightarrow> 'a::t2_space \<Rightarrow> 'b::real_normed_vector"
     1.9 -  assumes f: "\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)" shows "continuous F (\<lambda>x. \<Sum>i\<in>I. f i x)"
    1.10 -proof cases
    1.11 -  assume "finite I" from this f show ?thesis
    1.12 -    by (induct I) (auto intro!: continuous_intros)
    1.13 -qed (auto intro!: continuous_intros)
    1.14 -
    1.15  lemma brouwer_compactness_lemma:
    1.16    fixes f :: "'a::metric_space \<Rightarrow> 'b::euclidean_space"
    1.17    assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = 0))"