equal
deleted
inserted
replaced
242 instance |
242 instance |
243 by standard (auto intro!: bcontfun_eqI simp: algebra_simps) |
243 by standard (auto intro!: bcontfun_eqI simp: algebra_simps) |
244 |
244 |
245 end |
245 end |
246 |
246 |
247 lemma bounded_norm_le_SUP_norm: |
|
248 "bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))" |
|
249 by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp) |
|
250 |
|
251 instantiation\<^marker>\<open>tag unimportant\<close> bcontfun :: (topological_space, real_normed_vector) real_normed_vector |
247 instantiation\<^marker>\<open>tag unimportant\<close> bcontfun :: (topological_space, real_normed_vector) real_normed_vector |
252 begin |
248 begin |
253 |
249 |
254 definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real" |
250 definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real" |
255 where "norm_bcontfun f = dist f 0" |
251 where "norm_bcontfun f = dist f 0" |