2108 obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto |
2108 obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto |
2109 hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis a" in ballE) defer apply(erule_tac x="basis a" in ballE) |
2109 hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis a" in ballE) defer apply(erule_tac x="basis a" in ballE) |
2110 unfolding Ball_def mem_cball dist_norm by (auto simp add: norm_basis[unfolded One_nat_def]) |
2110 unfolding Ball_def mem_cball dist_norm by (auto simp add: norm_basis[unfolded One_nat_def]) |
2111 case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI) |
2111 case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI) |
2112 apply(rule) apply(rule divide_pos_pos) prefer 3 apply(rule,rule,erule conjE) |
2112 apply(rule) apply(rule divide_pos_pos) prefer 3 apply(rule,rule,erule conjE) |
2113 unfolding norm_0 scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel proof- |
2113 unfolding norm_zero scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel proof- |
2114 fix e and x::"real^'n" assume as:"norm x < e / B" "0 < norm x" "0<e" |
2114 fix e and x::"real^'n" assume as:"norm x < e / B" "0 < norm x" "0<e" |
2115 hence "surf (pi x) \<in> frontier s" using pi(1)[of x] unfolding surf(5)[THEN sym] by auto |
2115 hence "surf (pi x) \<in> frontier s" using pi(1)[of x] unfolding surf(5)[THEN sym] by auto |
2116 hence "norm (surf (pi x)) \<le> B" using B fs by auto |
2116 hence "norm (surf (pi x)) \<le> B" using B fs by auto |
2117 hence "norm x * norm (surf (pi x)) \<le> norm x * B" using as(2) by auto |
2117 hence "norm x * norm (surf (pi x)) \<le> norm x * B" using as(2) by auto |
2118 also have "\<dots> < e / B * B" apply(rule mult_strict_right_mono) using as(1) `B>0` by auto |
2118 also have "\<dots> < e / B * B" apply(rule mult_strict_right_mono) using as(1) `B>0` by auto |