equal
deleted
inserted
replaced
1244 then show ?thesis |
1244 then show ?thesis |
1245 proof cases |
1245 proof cases |
1246 case 1 |
1246 case 1 |
1247 show ?thesis |
1247 show ?thesis |
1248 by (rule negligible_subset [of "closure S"]) |
1248 by (rule negligible_subset [of "closure S"]) |
1249 (simp_all add: Diff_subset frontier_def negligible_lowdim 1) |
1249 (simp_all add: frontier_def negligible_lowdim 1) |
1250 next |
1250 next |
1251 case 2 |
1251 case 2 |
1252 obtain a where a: "a \<in> interior S" |
1252 obtain a where a: "a \<in> interior S" |
1253 apply (rule interior_simplex_nonempty [OF indB]) |
1253 apply (rule interior_simplex_nonempty [OF indB]) |
1254 apply (simp add: indB independent_finite) |
1254 apply (simp add: indB independent_finite) |