equal
deleted
inserted
replaced
305 by auto |
305 by auto |
306 then show ?thesis |
306 then show ?thesis |
307 proof (intro bcontfunI) |
307 proof (intro bcontfunI) |
308 fix x |
308 fix x |
309 assume "\<And>x. dist (f x) 0 \<le> y" |
309 assume "\<And>x. dist (f x) 0 \<le> y" |
310 then show "dist (a *\<^sub>R f x) 0 \<le> abs a * y" |
310 then show "dist (a *\<^sub>R f x) 0 \<le> \<bar>a\<bar> * y" |
311 by (metis norm_cmul_rule_thm norm_conv_dist) |
311 by (metis norm_cmul_rule_thm norm_conv_dist) |
312 qed (simp add: continuous_intros) |
312 qed (simp add: continuous_intros) |
313 qed |
313 qed |
314 |
314 |
315 lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x" |
315 lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x" |