89 apply (rule continuous_intros *)+ |
89 apply (rule continuous_intros *)+ |
90 using ss_pos apply force |
90 using ss_pos apply force |
91 done |
91 done |
92 qed |
92 qed |
93 moreover have "\<lbrakk>U \<in> \<C>; x \<in> S\<rbrakk> \<Longrightarrow> 0 \<le> F U x" for U x |
93 moreover have "\<lbrakk>U \<in> \<C>; x \<in> S\<rbrakk> \<Longrightarrow> 0 \<le> F U x" for U x |
94 using nonneg [of x] by (simp add: F_def divide_simps setdist_pos_le) |
94 using nonneg [of x] by (simp add: F_def field_split_simps setdist_pos_le) |
95 ultimately show "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x\<in>S. 0 \<le> F U x)" |
95 ultimately show "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x\<in>S. 0 \<le> F U x)" |
96 by metis |
96 by metis |
97 next |
97 next |
98 show "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0" |
98 show "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0" |
99 by (simp add: setdist_eq_0_sing_1 closure_def F_def) |
99 by (simp add: setdist_eq_0_sing_1 closure_def F_def) |
100 next |
100 next |
101 show "supp_sum (\<lambda>W. F W x) \<C> = 1" if "x \<in> S" for x |
101 show "supp_sum (\<lambda>W. F W x) \<C> = 1" if "x \<in> S" for x |
102 using that ss_pos [OF that] |
102 using that ss_pos [OF that] |
103 by (simp add: F_def divide_simps supp_sum_divide_distrib [symmetric]) |
103 by (simp add: F_def field_split_simps supp_sum_divide_distrib [symmetric]) |
104 next |
104 next |
105 show "\<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}" if "x \<in> S" for x |
105 show "\<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}" if "x \<in> S" for x |
106 using fin [OF that] that |
106 using fin [OF that] that |
107 by (fastforce simp: setdist_eq_0_sing_1 closure_def F_def elim!: rev_finite_subset) |
107 by (fastforce simp: setdist_eq_0_sing_1 closure_def F_def elim!: rev_finite_subset) |
108 qed |
108 qed |
155 apply (rule iffI) |
155 apply (rule iffI) |
156 apply (metis \<open>a \<noteq> b\<close> add_diff_cancel_left' eq_iff_diff_eq_0 pth_1 real_vector.scale_right_imp_eq, force) |
156 apply (metis \<open>a \<noteq> b\<close> add_diff_cancel_left' eq_iff_diff_eq_0 pth_1 real_vector.scale_right_imp_eq, force) |
157 done |
157 done |
158 also have "... \<longleftrightarrow> setdist {x} T = 0 \<and> setdist {x} S \<noteq> 0" |
158 also have "... \<longleftrightarrow> setdist {x} T = 0 \<and> setdist {x} S \<noteq> 0" |
159 using sdpos that |
159 using sdpos that |
160 by (simp add: divide_simps) linarith |
160 by (simp add: field_split_simps) linarith |
161 also have "... \<longleftrightarrow> x \<in> T" |
161 also have "... \<longleftrightarrow> x \<in> T" |
162 using \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>S \<inter> T = {}\<close> that |
162 using \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>S \<inter> T = {}\<close> that |
163 by (force simp: S0 T0) |
163 by (force simp: S0 T0) |
164 finally show ?thesis . |
164 finally show ?thesis . |
165 qed |
165 qed |