equal
deleted
inserted
replaced
7 subsection \<open>Definition\<close> |
7 subsection \<open>Definition\<close> |
8 |
8 |
9 definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set" |
9 definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set" |
10 where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}" |
10 where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}" |
11 |
11 |
12 typedef ('a, 'b) bcontfun = "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set" |
12 typedef (overloaded) ('a, 'b) bcontfun = |
|
13 "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set" |
13 by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def) |
14 by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def) |
14 |
15 |
15 lemma bcontfunE: |
16 lemma bcontfunE: |
16 assumes "f \<in> bcontfun" |
17 assumes "f \<in> bcontfun" |
17 obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) u \<le> y" |
18 obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) u \<le> y" |