equal
deleted
inserted
replaced
33 assume "finite I" from this f show ?thesis |
33 assume "finite I" from this f show ?thesis |
34 by (induct I) (auto intro!: continuous_intros) |
34 by (induct I) (auto intro!: continuous_intros) |
35 qed (auto intro!: continuous_intros) |
35 qed (auto intro!: continuous_intros) |
36 |
36 |
37 lemma brouwer_compactness_lemma: |
37 lemma brouwer_compactness_lemma: |
38 assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = (0::_::euclidean_space)))" |
38 fixes f :: "'a::metric_space \<Rightarrow> 'b::euclidean_space" |
|
39 assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = 0))" |
39 obtains d where "0 < d" "\<forall>x\<in>s. d \<le> norm(f x)" |
40 obtains d where "0 < d" "\<forall>x\<in>s. d \<le> norm(f x)" |
40 proof (cases "s={}") |
41 proof (cases "s={}") |
41 case False |
42 case False |
42 have "continuous_on s (norm \<circ> f)" |
43 have "continuous_on s (norm \<circ> f)" |
43 by (rule continuous_on_intros continuous_on_norm assms(2))+ |
44 by (rule continuous_on_intros continuous_on_norm assms(2))+ |