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))"
```