1 section \<open>Bounded Continuous Functions\<close> |
1 section \<open>Bounded Continuous Functions\<close> |
2 |
2 |
3 theory Bounded_Continuous_Function |
3 theory Bounded_Continuous_Function |
4 imports Henstock_Kurzweil_Integration |
4 imports |
|
5 Henstock_Kurzweil_Integration |
5 begin |
6 begin |
6 |
7 |
7 subsection \<open>Definition\<close> |
8 subsection \<open>Definition\<close> |
8 |
9 |
9 definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set" |
10 definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set" |
10 where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}" |
11 where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}" |
11 |
12 |
12 typedef (overloaded) ('a, 'b) bcontfun = |
13 typedef (overloaded) ('a, 'b) bcontfun ("(_ \<Rightarrow>\<^sub>C /_)" [22, 21] 21) = |
13 "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set" |
14 "{f::'a::topological_space \<Rightarrow> 'b::metric_space. continuous_on UNIV f \<and> bounded (range f)}" |
14 by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def) |
15 morphisms apply_bcontfun Bcontfun |
|
16 by (auto intro: continuous_intros simp: bounded_def) |
|
17 |
|
18 declare [[coercion "apply_bcontfun :: ('a::topological_space \<Rightarrow>\<^sub>C'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'b"]] |
|
19 |
|
20 setup_lifting type_definition_bcontfun |
|
21 |
|
22 lemma continuous_on_apply_bcontfun[intro, simp]: "continuous_on T (apply_bcontfun x)" |
|
23 and bounded_apply_bcontfun[intro, simp]: "bounded (range (apply_bcontfun x))" |
|
24 using apply_bcontfun[of x] |
|
25 by (auto simp: intro: continuous_on_subset) |
|
26 |
|
27 lemma bcontfun_eqI: "(\<And>x. apply_bcontfun f x = apply_bcontfun g x) \<Longrightarrow> f = g" |
|
28 by transfer auto |
15 |
29 |
16 lemma bcontfunE: |
30 lemma bcontfunE: |
17 assumes "f \<in> bcontfun" |
31 assumes "continuous_on UNIV f" "bounded (range f)" |
18 obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) u \<le> y" |
32 obtains g where "f = apply_bcontfun g" |
19 using assms unfolding bcontfun_def |
33 by (blast intro: apply_bcontfun_cases assms) |
20 by (metis (lifting) bounded_any_center dist_commute mem_Collect_eq rangeI) |
34 |
21 |
35 lift_definition const_bcontfun::"'b::metric_space \<Rightarrow> ('a::topological_space \<Rightarrow>\<^sub>C 'b)" is "\<lambda>c _. c" |
22 lemma bcontfunE': |
36 by (auto intro!: continuous_intros simp: image_def) |
23 assumes "f \<in> bcontfun" |
|
24 obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y" |
|
25 using assms bcontfunE |
|
26 by metis |
|
27 |
|
28 lemma bcontfunI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) u \<le> b) \<Longrightarrow> f \<in> bcontfun" |
|
29 unfolding bcontfun_def |
|
30 by (metis (lifting, no_types) bounded_def dist_commute mem_Collect_eq rangeE) |
|
31 |
|
32 lemma bcontfunI': "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) undefined \<le> b) \<Longrightarrow> f \<in> bcontfun" |
|
33 using bcontfunI by metis |
|
34 |
|
35 lemma continuous_on_Rep_bcontfun[intro, simp]: "continuous_on T (Rep_bcontfun x)" |
|
36 using Rep_bcontfun[of x] |
|
37 by (auto simp: bcontfun_def intro: continuous_on_subset) |
|
38 |
37 |
39 (* TODO: Generalize to uniform spaces? *) |
38 (* TODO: Generalize to uniform spaces? *) |
40 instantiation bcontfun :: (topological_space, metric_space) metric_space |
39 instantiation bcontfun :: (topological_space, metric_space) metric_space |
41 begin |
40 begin |
42 |
41 |
43 definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real" |
42 lift_definition dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real" |
44 where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))" |
43 is "\<lambda>f g. (SUP x. dist (f x) (g x))" . |
45 |
44 |
46 definition uniformity_bcontfun :: "(('a, 'b) bcontfun \<times> ('a, 'b) bcontfun) filter" |
45 definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter" |
47 where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})" |
46 where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})" |
48 |
47 |
49 definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool" |
48 definition open_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b) set \<Rightarrow> bool" |
50 where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)" |
49 where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)" |
51 |
50 |
|
51 lemma bounded_dist_le_SUP_dist: |
|
52 "bounded (range f) \<Longrightarrow> bounded (range g) \<Longrightarrow> dist (f x) (g x) \<le> (SUP x. dist (f x) (g x))" |
|
53 by (auto intro!: cSUP_upper bounded_imp_bdd_above bounded_dist_comp) |
|
54 |
52 lemma dist_bounded: |
55 lemma dist_bounded: |
53 fixes f :: "('a, 'b) bcontfun" |
56 fixes f g :: "'a \<Rightarrow>\<^sub>C 'b" |
54 shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g" |
57 shows "dist (f x) (g x) \<le> dist f g" |
55 proof - |
58 by transfer (auto intro!: bounded_dist_le_SUP_dist) |
56 have "Rep_bcontfun f \<in> bcontfun" by (rule Rep_bcontfun) |
|
57 from bcontfunE'[OF this] obtain y where y: |
|
58 "continuous_on UNIV (Rep_bcontfun f)" |
|
59 "\<And>x. dist (Rep_bcontfun f x) undefined \<le> y" |
|
60 by auto |
|
61 have "Rep_bcontfun g \<in> bcontfun" by (rule Rep_bcontfun) |
|
62 from bcontfunE'[OF this] obtain z where z: |
|
63 "continuous_on UNIV (Rep_bcontfun g)" |
|
64 "\<And>x. dist (Rep_bcontfun g x) undefined \<le> z" |
|
65 by auto |
|
66 show ?thesis |
|
67 unfolding dist_bcontfun_def |
|
68 proof (intro cSUP_upper bdd_aboveI2) |
|
69 fix x |
|
70 have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> |
|
71 dist (Rep_bcontfun f x) undefined + dist (Rep_bcontfun g x) undefined" |
|
72 by (rule dist_triangle2) |
|
73 also have "\<dots> \<le> y + z" |
|
74 using y(2)[of x] z(2)[of x] by (rule add_mono) |
|
75 finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> y + z" . |
|
76 qed simp |
|
77 qed |
|
78 |
59 |
79 lemma dist_bound: |
60 lemma dist_bound: |
80 fixes f :: "('a, 'b) bcontfun" |
61 fixes f g :: "'a \<Rightarrow>\<^sub>C 'b" |
81 assumes "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> b" |
62 assumes "\<And>x. dist (f x) (g x) \<le> b" |
82 shows "dist f g \<le> b" |
63 shows "dist f g \<le> b" |
83 using assms by (auto simp: dist_bcontfun_def intro: cSUP_least) |
64 using assms |
84 |
65 by transfer (auto intro!: cSUP_least) |
85 lemma dist_bounded_Abs: |
|
86 fixes f g :: "'a \<Rightarrow> 'b" |
|
87 assumes "f \<in> bcontfun" "g \<in> bcontfun" |
|
88 shows "dist (f x) (g x) \<le> dist (Abs_bcontfun f) (Abs_bcontfun g)" |
|
89 by (metis Abs_bcontfun_inverse assms dist_bounded) |
|
90 |
|
91 lemma const_bcontfun: "(\<lambda>x::'a. b::'b) \<in> bcontfun" |
|
92 by (auto intro: bcontfunI continuous_on_const) |
|
93 |
66 |
94 lemma dist_fun_lt_imp_dist_val_lt: |
67 lemma dist_fun_lt_imp_dist_val_lt: |
|
68 fixes f g :: "'a \<Rightarrow>\<^sub>C 'b" |
95 assumes "dist f g < e" |
69 assumes "dist f g < e" |
96 shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e" |
70 shows "dist (f x) (g x) < e" |
97 using dist_bounded assms by (rule le_less_trans) |
71 using dist_bounded assms by (rule le_less_trans) |
98 |
|
99 lemma dist_val_lt_imp_dist_fun_le: |
|
100 assumes "\<forall>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e" |
|
101 shows "dist f g \<le> e" |
|
102 unfolding dist_bcontfun_def |
|
103 proof (intro cSUP_least) |
|
104 fix x |
|
105 show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> e" |
|
106 using assms[THEN spec[where x=x]] by (simp add: dist_norm) |
|
107 qed simp |
|
108 |
72 |
109 instance |
73 instance |
110 proof |
74 proof |
111 fix f g h :: "('a, 'b) bcontfun" |
75 fix f g h :: "'a \<Rightarrow>\<^sub>C 'b" |
112 show "dist f g = 0 \<longleftrightarrow> f = g" |
76 show "dist f g = 0 \<longleftrightarrow> f = g" |
113 proof |
77 proof |
114 have "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g" |
78 have "\<And>x. dist (f x) (g x) \<le> dist f g" |
115 by (rule dist_bounded) |
79 by (rule dist_bounded) |
116 also assume "dist f g = 0" |
80 also assume "dist f g = 0" |
117 finally show "f = g" |
81 finally show "f = g" |
118 by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse) |
82 by (auto simp: apply_bcontfun_inject[symmetric]) |
119 qed (auto simp: dist_bcontfun_def intro!: cSup_eq) |
83 qed (auto simp: dist_bcontfun_def intro!: cSup_eq) |
120 show "dist f g \<le> dist f h + dist g h" |
84 show "dist f g \<le> dist f h + dist g h" |
121 proof (subst dist_bcontfun_def, safe intro!: cSUP_least) |
85 proof (rule dist_bound) |
122 fix x |
86 fix x |
123 have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> |
87 have "dist (f x) (g x) \<le> dist (f x) (h x) + dist (g x) (h x)" |
124 dist (Rep_bcontfun f x) (Rep_bcontfun h x) + dist (Rep_bcontfun g x) (Rep_bcontfun h x)" |
|
125 by (rule dist_triangle2) |
88 by (rule dist_triangle2) |
126 also have "dist (Rep_bcontfun f x) (Rep_bcontfun h x) \<le> dist f h" |
89 also have "dist (f x) (h x) \<le> dist f h" |
127 by (rule dist_bounded) |
90 by (rule dist_bounded) |
128 also have "dist (Rep_bcontfun g x) (Rep_bcontfun h x) \<le> dist g h" |
91 also have "dist (g x) (h x) \<le> dist g h" |
129 by (rule dist_bounded) |
92 by (rule dist_bounded) |
130 finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h" |
93 finally show "dist (f x) (g x) \<le> dist f h + dist g h" |
131 by simp |
94 by simp |
132 qed |
95 qed |
133 qed (rule open_bcontfun_def uniformity_bcontfun_def)+ |
96 qed (rule open_bcontfun_def uniformity_bcontfun_def)+ |
134 |
97 |
135 end |
98 end |
136 |
99 |
137 lemma closed_Pi_bcontfun: |
100 lift_definition PiC::"'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b::metric_space) set" |
|
101 is "\<lambda>I X. Pi I X \<inter> {f. continuous_on UNIV f \<and> bounded (range f)}" |
|
102 by auto |
|
103 |
|
104 lemma mem_PiC_iff: "x \<in> PiC I X \<longleftrightarrow> apply_bcontfun x \<in> Pi I X" |
|
105 by transfer simp |
|
106 |
|
107 lemmas mem_PiCD = mem_PiC_iff[THEN iffD1] |
|
108 and mem_PiCI = mem_PiC_iff[THEN iffD2] |
|
109 |
|
110 lemma tendsto_bcontfun_uniform_limit: |
|
111 fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space" |
|
112 assumes "(f \<longlongrightarrow> l) F" |
|
113 shows "uniform_limit UNIV f l F" |
|
114 proof (rule uniform_limitI) |
|
115 fix e::real assume "e > 0" |
|
116 from tendstoD[OF assms this] have "\<forall>\<^sub>F x in F. dist (f x) l < e" . |
|
117 then show "\<forall>\<^sub>F n in F. \<forall>x\<in>UNIV. dist ((f n) x) (l x) < e" |
|
118 by eventually_elim (auto simp: dist_fun_lt_imp_dist_val_lt) |
|
119 qed |
|
120 |
|
121 lemma uniform_limit_tendsto_bcontfun: |
|
122 fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space" |
|
123 and l::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space" |
|
124 assumes "uniform_limit UNIV f l F" |
|
125 shows "(f \<longlongrightarrow> l) F" |
|
126 proof (rule tendstoI) |
|
127 fix e::real assume "e > 0" |
|
128 then have "e / 2 > 0" by simp |
|
129 from uniform_limitD[OF assms this] |
|
130 have "\<forall>\<^sub>F i in F. \<forall>x. dist (f i x) (l x) < e / 2" by simp |
|
131 then have "\<forall>\<^sub>F x in F. dist (f x) l \<le> e / 2" |
|
132 by eventually_elim (blast intro: dist_bound less_imp_le) |
|
133 then show "\<forall>\<^sub>F x in F. dist (f x) l < e" |
|
134 by eventually_elim (use \<open>0 < e\<close> in auto) |
|
135 qed |
|
136 |
|
137 lemma uniform_limit_bcontfunE: |
|
138 fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space" |
|
139 and l::"'a::topological_space \<Rightarrow> 'b::metric_space" |
|
140 assumes "uniform_limit UNIV f l F" "F \<noteq> bot" |
|
141 obtains l'::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space" |
|
142 where "l = l'" "(f \<longlongrightarrow> l') F" |
|
143 by (metis (mono_tags, lifting) always_eventually apply_bcontfun apply_bcontfun_cases assms |
|
144 mem_Collect_eq uniform_limit_bounded uniform_limit_tendsto_bcontfun uniform_limit_theorem) |
|
145 |
|
146 lemma closed_PiC: |
138 fixes I :: "'a::metric_space set" |
147 fixes I :: "'a::metric_space set" |
139 and X :: "'a \<Rightarrow> 'b::complete_space set" |
148 and X :: "'a \<Rightarrow> 'b::complete_space set" |
140 assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)" |
149 assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)" |
141 shows "closed (Abs_bcontfun ` (Pi I X \<inter> bcontfun))" |
150 shows "closed (PiC I X)" |
142 unfolding closed_sequential_limits |
151 unfolding closed_sequential_limits |
143 proof safe |
152 proof safe |
144 fix f l |
153 fix f l |
145 assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f \<longlonglongrightarrow> l" |
154 assume seq: "\<forall>n. f n \<in> PiC I X" and lim: "f \<longlonglongrightarrow> l" |
146 have lim_fun: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (Rep_bcontfun l x) < e" |
155 show "l \<in> PiC I X" |
147 using LIMSEQ_imp_Cauchy[OF lim, simplified Cauchy_def] metric_LIMSEQ_D[OF lim] |
156 proof (safe intro!: mem_PiCI) |
148 by (intro uniformly_cauchy_imp_uniformly_convergent[where P="\<lambda>_. True", simplified]) |
|
149 (metis dist_fun_lt_imp_dist_val_lt)+ |
|
150 show "l \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" |
|
151 proof (rule, safe) |
|
152 fix x assume "x \<in> I" |
157 fix x assume "x \<in> I" |
153 then have "closed (X x)" |
158 then have "closed (X x)" |
154 using assms by simp |
159 using assms by simp |
155 moreover have "eventually (\<lambda>xa. Rep_bcontfun (f xa) x \<in> X x) sequentially" |
160 moreover have "eventually (\<lambda>i. f i x \<in> X x) sequentially" |
156 proof (rule always_eventually, safe) |
161 using seq \<open>x \<in> I\<close> |
157 fix i |
162 by (auto intro!: eventuallyI dest!: mem_PiCD simp: Pi_iff) |
158 from seq[THEN spec, of i] \<open>x \<in> I\<close> |
|
159 show "Rep_bcontfun (f i) x \<in> X x" |
|
160 by (auto simp: Abs_bcontfun_inverse) |
|
161 qed |
|
162 moreover note sequentially_bot |
163 moreover note sequentially_bot |
163 moreover have "(\<lambda>n. Rep_bcontfun (f n) x) \<longlonglongrightarrow> Rep_bcontfun l x" |
164 moreover have "(\<lambda>n. (f n) x) \<longlonglongrightarrow> l x" |
164 using lim_fun by (blast intro!: metric_LIMSEQ_I) |
165 using tendsto_bcontfun_uniform_limit[OF lim] |
165 ultimately show "Rep_bcontfun l x \<in> X x" |
166 by (rule tendsto_uniform_limitI) simp |
|
167 ultimately show "l x \<in> X x" |
166 by (rule Lim_in_closed_set) |
168 by (rule Lim_in_closed_set) |
167 qed (auto simp: Rep_bcontfun Rep_bcontfun_inverse) |
169 qed |
168 qed |
170 qed |
169 |
171 |
170 |
172 |
171 subsection \<open>Complete Space\<close> |
173 subsection \<open>Complete Space\<close> |
172 |
174 |
173 instance bcontfun :: (metric_space, complete_space) complete_space |
175 instance bcontfun :: (metric_space, complete_space) complete_space |
174 proof |
176 proof |
175 fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun" |
177 fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun" |
176 assume "Cauchy f" \<comment> \<open>Cauchy equals uniform convergence\<close> |
178 assume "Cauchy f" \<comment> \<open>Cauchy equals uniform convergence\<close> |
177 then obtain g where limit_function: |
179 then obtain g where "uniform_limit UNIV f g sequentially" |
178 "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e" |
180 using uniformly_convergent_eq_cauchy[of "\<lambda>_. True" f] |
179 using uniformly_convergent_eq_cauchy[of "\<lambda>_. True" |
181 unfolding Cauchy_def uniform_limit_sequentially_iff |
180 "\<lambda>n. Rep_bcontfun (f n)"] |
|
181 unfolding Cauchy_def |
|
182 by (metis dist_fun_lt_imp_dist_val_lt) |
182 by (metis dist_fun_lt_imp_dist_val_lt) |
183 |
183 |
184 then obtain N where fg_dist: \<comment> \<open>for an upper bound on @{term g}\<close> |
184 from uniform_limit_bcontfunE[OF this sequentially_bot] |
185 "\<forall>n\<ge>N. \<forall>x. dist (g x) ( Rep_bcontfun (f n) x) < 1" |
185 obtain l' where "g = apply_bcontfun l'" "(f \<longlonglongrightarrow> l')" by metis |
186 by (force simp add: dist_commute) |
186 then show "convergent f" |
187 from bcontfunE'[OF Rep_bcontfun, of "f N"] obtain b where |
187 by (intro convergentI) |
188 f_bound: "\<forall>x. dist (Rep_bcontfun (f N) x) undefined \<le> b" |
|
189 by force |
|
190 have "g \<in> bcontfun" \<comment> \<open>The limit function is bounded and continuous\<close> |
|
191 proof (intro bcontfunI) |
|
192 show "continuous_on UNIV g" |
|
193 apply (rule bcontfunE[OF Rep_bcontfun]) |
|
194 using limit_function |
|
195 by (auto simp add: uniform_limit_sequentially_iff intro: uniform_limit_theorem[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"]) |
|
196 next |
|
197 fix x |
|
198 from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1" |
|
199 by (simp add: dist_norm norm_minus_commute) |
|
200 with dist_triangle[of "g x" undefined "Rep_bcontfun (f N) x"] |
|
201 show "dist (g x) undefined \<le> 1 + b" using f_bound[THEN spec, of x] |
|
202 by simp |
|
203 qed |
|
204 show "convergent f" |
|
205 proof (rule convergentI, subst lim_sequentially, safe) |
|
206 \<comment> \<open>The limit function converges according to its norm\<close> |
|
207 fix e :: real |
|
208 assume "e > 0" |
|
209 then have "e/2 > 0" by simp |
|
210 with limit_function[THEN spec, of"e/2"] |
|
211 have "\<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e/2" |
|
212 by simp |
|
213 then obtain N where N: "\<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e / 2" by auto |
|
214 show "\<exists>N. \<forall>n\<ge>N. dist (f n) (Abs_bcontfun g) < e" |
|
215 proof (rule, safe) |
|
216 fix n |
|
217 assume "N \<le> n" |
|
218 with N show "dist (f n) (Abs_bcontfun g) < e" |
|
219 using dist_val_lt_imp_dist_fun_le[of |
|
220 "f n" "Abs_bcontfun g" "e/2"] |
|
221 Abs_bcontfun_inverse[OF \<open>g \<in> bcontfun\<close>] \<open>e > 0\<close> by simp |
|
222 qed |
|
223 qed |
|
224 qed |
188 qed |
225 |
189 |
226 |
190 |
227 subsection \<open>Supremum norm for a normed vector space\<close> |
191 subsection \<open>Supremum norm for a normed vector space\<close> |
228 |
192 |
229 instantiation bcontfun :: (topological_space, real_normed_vector) real_vector |
193 instantiation bcontfun :: (topological_space, real_normed_vector) real_vector |
230 begin |
194 begin |
231 |
195 |
232 definition "-f = Abs_bcontfun (\<lambda>x. -(Rep_bcontfun f x))" |
196 lift_definition uminus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>f x. - f x" |
233 |
197 by (auto intro!: continuous_intros) |
234 definition "f + g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x + Rep_bcontfun g x)" |
198 |
235 |
199 lift_definition plus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>f g x. f x + g x" |
236 definition "f - g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x - Rep_bcontfun g x)" |
200 by (auto simp: intro!: continuous_intros bounded_plus_comp) |
237 |
201 |
238 definition "0 = Abs_bcontfun (\<lambda>x. 0)" |
202 lift_definition minus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>f g x. f x - g x" |
239 |
203 by (auto simp: intro!: continuous_intros bounded_minus_comp) |
240 definition "scaleR r f = Abs_bcontfun (\<lambda>x. r *\<^sub>R Rep_bcontfun f x)" |
204 |
241 |
205 lift_definition zero_bcontfun::"'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>_. 0" |
242 lemma plus_cont: |
206 by (auto intro!: continuous_intros simp: image_def) |
243 fixes f g :: "'a \<Rightarrow> 'b" |
207 |
244 assumes f: "f \<in> bcontfun" |
208 lemma const_bcontfun_0_eq_0[simp]: "const_bcontfun 0 = 0" |
245 and g: "g \<in> bcontfun" |
209 by transfer simp |
246 shows "(\<lambda>x. f x + g x) \<in> bcontfun" |
210 |
247 proof - |
211 lift_definition scaleR_bcontfun::"real \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>r g x. r *\<^sub>R g x" |
248 from bcontfunE'[OF f] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y" |
212 by (auto simp: intro!: continuous_intros bounded_scaleR_comp) |
249 by auto |
213 |
250 moreover |
214 lemmas [simp] = |
251 from bcontfunE'[OF g] obtain z where "continuous_on UNIV g" "\<And>x. dist (g x) undefined \<le> z" |
215 const_bcontfun.rep_eq |
252 by auto |
216 uminus_bcontfun.rep_eq |
253 ultimately show ?thesis |
217 plus_bcontfun.rep_eq |
254 proof (intro bcontfunI) |
218 minus_bcontfun.rep_eq |
255 fix x |
219 zero_bcontfun.rep_eq |
256 have "dist (f x + g x) 0 = dist (f x + g x) (0 + 0)" |
220 scaleR_bcontfun.rep_eq |
257 by simp |
221 |
258 also have "\<dots> \<le> dist (f x) 0 + dist (g x) 0" |
|
259 by (rule dist_triangle_add) |
|
260 also have "\<dots> \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" |
|
261 unfolding zero_bcontfun_def using assms |
|
262 by (metis add_mono const_bcontfun dist_bounded_Abs) |
|
263 finally show "dist (f x + g x) 0 \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" . |
|
264 qed (simp add: continuous_on_add) |
|
265 qed |
|
266 |
|
267 lemma Rep_bcontfun_plus[simp]: "Rep_bcontfun (f + g) x = Rep_bcontfun f x + Rep_bcontfun g x" |
|
268 by (simp add: plus_bcontfun_def Abs_bcontfun_inverse plus_cont Rep_bcontfun) |
|
269 |
|
270 lemma uminus_cont: |
|
271 fixes f :: "'a \<Rightarrow> 'b" |
|
272 assumes "f \<in> bcontfun" |
|
273 shows "(\<lambda>x. - f x) \<in> bcontfun" |
|
274 proof - |
|
275 from bcontfunE[OF assms, of 0] obtain y |
|
276 where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y" |
|
277 by auto |
|
278 then show ?thesis |
|
279 proof (intro bcontfunI) |
|
280 fix x |
|
281 assume "\<And>x. dist (f x) 0 \<le> y" |
|
282 then show "dist (- f x) 0 \<le> y" |
|
283 by (subst dist_minus[symmetric]) simp |
|
284 qed (simp add: continuous_on_minus) |
|
285 qed |
|
286 |
|
287 lemma Rep_bcontfun_uminus[simp]: "Rep_bcontfun (- f) x = - Rep_bcontfun f x" |
|
288 by (simp add: uminus_bcontfun_def Abs_bcontfun_inverse uminus_cont Rep_bcontfun) |
|
289 |
|
290 lemma minus_cont: |
|
291 fixes f g :: "'a \<Rightarrow> 'b" |
|
292 assumes f: "f \<in> bcontfun" |
|
293 and g: "g \<in> bcontfun" |
|
294 shows "(\<lambda>x. f x - g x) \<in> bcontfun" |
|
295 using plus_cont [of f "- g"] assms |
|
296 by (simp add: uminus_cont fun_Compl_def) |
|
297 |
|
298 lemma Rep_bcontfun_minus[simp]: "Rep_bcontfun (f - g) x = Rep_bcontfun f x - Rep_bcontfun g x" |
|
299 by (simp add: minus_bcontfun_def Abs_bcontfun_inverse minus_cont Rep_bcontfun) |
|
300 |
|
301 lemma scaleR_cont: |
|
302 fixes a :: real |
|
303 and f :: "'a \<Rightarrow> 'b" |
|
304 assumes "f \<in> bcontfun" |
|
305 shows " (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun" |
|
306 proof - |
|
307 from bcontfunE[OF assms, of 0] obtain y |
|
308 where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y" |
|
309 by auto |
|
310 then show ?thesis |
|
311 proof (intro bcontfunI) |
|
312 fix x |
|
313 assume "\<And>x. dist (f x) 0 \<le> y" |
|
314 then show "dist (a *\<^sub>R f x) 0 \<le> \<bar>a\<bar> * y" |
|
315 by (metis norm_cmul_rule_thm norm_conv_dist) |
|
316 qed (simp add: continuous_intros) |
|
317 qed |
|
318 |
|
319 lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x" |
|
320 by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun) |
|
321 |
222 |
322 instance |
223 instance |
323 by standard |
224 by standard (auto intro!: bcontfun_eqI simp: algebra_simps) |
324 (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def |
|
325 Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps |
|
326 plus_cont const_bcontfun minus_cont scaleR_cont) |
|
327 |
225 |
328 end |
226 end |
|
227 |
|
228 lemma bounded_norm_le_SUP_norm: |
|
229 "bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))" |
|
230 by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp) |
329 |
231 |
330 instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector |
232 instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector |
331 begin |
233 begin |
332 |
234 |
333 definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real" |
235 definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real" |
338 instance |
240 instance |
339 proof |
241 proof |
340 fix a :: real |
242 fix a :: real |
341 fix f g :: "('a, 'b) bcontfun" |
243 fix f g :: "('a, 'b) bcontfun" |
342 show "dist f g = norm (f - g)" |
244 show "dist f g = norm (f - g)" |
343 by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def |
245 unfolding norm_bcontfun_def |
344 Abs_bcontfun_inverse const_bcontfun dist_norm) |
246 by transfer (simp add: dist_norm) |
345 show "norm (f + g) \<le> norm f + norm g" |
247 show "norm (f + g) \<le> norm f + norm g" |
346 unfolding norm_bcontfun_def |
248 unfolding norm_bcontfun_def |
347 proof (subst dist_bcontfun_def, safe intro!: cSUP_least) |
249 by transfer |
348 fix x |
250 (auto intro!: cSUP_least norm_triangle_le add_mono bounded_norm_le_SUP_norm simp: dist_norm) |
349 have "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> |
|
350 dist (Rep_bcontfun f x) 0 + dist (Rep_bcontfun g x) 0" |
|
351 by (metis (hide_lams, no_types) Rep_bcontfun_minus Rep_bcontfun_plus diff_0_right dist_norm |
|
352 le_less_linear less_irrefl norm_triangle_lt) |
|
353 also have "dist (Rep_bcontfun f x) 0 \<le> dist f 0" |
|
354 using dist_bounded[of f x 0] |
|
355 by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def) |
|
356 also have "dist (Rep_bcontfun g x) 0 \<le> dist g 0" using dist_bounded[of g x 0] |
|
357 by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def) |
|
358 finally show "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> dist f 0 + dist g 0" by simp |
|
359 qed |
|
360 show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f" |
251 show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f" |
361 proof - |
252 unfolding norm_bcontfun_def |
362 have "\<bar>a\<bar> * Sup (range (\<lambda>x. dist (Rep_bcontfun f x) 0)) = |
253 apply transfer |
363 (SUP i:range (\<lambda>x. dist (Rep_bcontfun f x) 0). \<bar>a\<bar> * i)" |
254 by (rule trans[OF _ continuous_at_Sup_mono[symmetric]]) |
364 proof (intro continuous_at_Sup_mono bdd_aboveI2) |
255 (auto intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above |
365 fix x |
256 simp: bounded_norm_comp) |
366 show "dist (Rep_bcontfun f x) 0 \<le> norm f" using dist_bounded[of f x 0] |
|
367 by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def |
|
368 const_bcontfun) |
|
369 qed (auto intro!: monoI mult_left_mono continuous_intros) |
|
370 moreover |
|
371 have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) = |
|
372 (\<lambda>x. \<bar>a\<bar> * x) ` (range (\<lambda>x. dist (Rep_bcontfun f x) 0))" |
|
373 by auto |
|
374 ultimately |
|
375 show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f" |
|
376 by (simp add: norm_bcontfun_def dist_bcontfun_def Abs_bcontfun_inverse |
|
377 zero_bcontfun_def const_bcontfun image_image) |
|
378 qed |
|
379 qed (auto simp: norm_bcontfun_def sgn_bcontfun_def) |
257 qed (auto simp: norm_bcontfun_def sgn_bcontfun_def) |
380 |
258 |
381 end |
259 end |
382 |
|
383 lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun" |
|
384 by (metis bcontfunI dist_0_norm dist_commute) |
|
385 |
260 |
386 lemma norm_bounded: |
261 lemma norm_bounded: |
387 fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun" |
262 fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun" |
388 shows "norm (Rep_bcontfun f x) \<le> norm f" |
263 shows "norm (apply_bcontfun f x) \<le> norm f" |
389 using dist_bounded[of f x 0] |
264 using dist_bounded[of f x 0] |
390 by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def |
265 by (simp add: dist_norm) |
391 const_bcontfun) |
|
392 |
266 |
393 lemma norm_bound: |
267 lemma norm_bound: |
394 fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun" |
268 fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun" |
395 assumes "\<And>x. norm (Rep_bcontfun f x) \<le> b" |
269 assumes "\<And>x. norm (apply_bcontfun f x) \<le> b" |
396 shows "norm f \<le> b" |
270 shows "norm f \<le> b" |
397 using dist_bound[of f 0 b] assms |
271 using dist_bound[of f 0 b] assms |
398 by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def const_bcontfun) |
272 by (simp add: dist_norm) |
399 |
273 |
400 |
274 subsection \<open>(bounded) continuous extenstion\<close> |
401 subsection \<open>Continuously Extended Functions\<close> |
|
402 |
|
403 definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where |
|
404 "clamp a b x = (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)" |
|
405 |
|
406 definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b) bcontfun" |
|
407 where "ext_cont f a b = Abs_bcontfun ((\<lambda>x. f (clamp a b x)))" |
|
408 |
|
409 lemma ext_cont_def': |
|
410 "ext_cont f a b = Abs_bcontfun (\<lambda>x. |
|
411 f (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i))" |
|
412 unfolding ext_cont_def clamp_def .. |
|
413 |
|
414 lemma clamp_in_interval: |
|
415 assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" |
|
416 shows "clamp a b x \<in> cbox a b" |
|
417 unfolding clamp_def |
|
418 using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def) |
|
419 |
|
420 lemma dist_clamps_le_dist_args: |
|
421 fixes x :: "'a::euclidean_space" |
|
422 assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" |
|
423 shows "dist (clamp a b y) (clamp a b x) \<le> dist y x" |
|
424 proof - |
|
425 from box_ne_empty(1)[of a b] assms have "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)" |
|
426 by (simp add: cbox_def) |
|
427 then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le> |
|
428 (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)" |
|
429 by (auto intro!: sum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric]) |
|
430 then show ?thesis |
|
431 by (auto intro: real_sqrt_le_mono |
|
432 simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def) |
|
433 qed |
|
434 |
|
435 lemma clamp_continuous_at: |
|
436 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space" |
|
437 and x :: 'a |
|
438 assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" |
|
439 and f_cont: "continuous_on (cbox a b) f" |
|
440 shows "continuous (at x) (\<lambda>x. f (clamp a b x))" |
|
441 unfolding continuous_at_eps_delta |
|
442 proof safe |
|
443 fix x :: 'a |
|
444 fix e :: real |
|
445 assume "e > 0" |
|
446 moreover have "clamp a b x \<in> cbox a b" |
|
447 by (simp add: clamp_in_interval assms) |
|
448 moreover note f_cont[simplified continuous_on_iff] |
|
449 ultimately |
|
450 obtain d where d: "0 < d" |
|
451 "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e" |
|
452 by force |
|
453 show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow> |
|
454 dist (f (clamp a b x')) (f (clamp a b x)) < e" |
|
455 by (auto intro!: d clamp_in_interval assms dist_clamps_le_dist_args[THEN le_less_trans]) |
|
456 qed |
|
457 |
|
458 lemma clamp_continuous_on: |
|
459 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space" |
|
460 assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" |
|
461 and f_cont: "continuous_on (cbox a b) f" |
|
462 shows "continuous_on UNIV (\<lambda>x. f (clamp a b x))" |
|
463 using assms |
|
464 by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at) |
|
465 |
|
466 lemma clamp_bcontfun: |
|
467 fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector" |
|
468 assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i" |
|
469 and continuous: "continuous_on (cbox a b) f" |
|
470 shows "(\<lambda>x. f (clamp a b x)) \<in> bcontfun" |
|
471 proof - |
|
472 have "bounded (f ` (cbox a b))" |
|
473 by (rule compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded]) |
|
474 then obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. norm x \<le> c" |
|
475 by (auto simp add: bounded_pos) |
|
476 show "(\<lambda>x. f (clamp a b x)) \<in> bcontfun" |
|
477 proof (intro bcontfun_normI) |
|
478 fix x |
|
479 show "norm (f (clamp a b x)) \<le> c" |
|
480 using clamp_in_interval[OF assms(1), of x] f_bound |
|
481 by (simp add: ext_cont_def) |
|
482 qed (simp add: clamp_continuous_on assms) |
|
483 qed |
|
484 |
275 |
485 lemma integral_clamp: |
276 lemma integral_clamp: |
486 "integral {t0::real..clamp t0 t1 x} f = |
277 "integral {t0::real..clamp t0 t1 x} f = |
487 (if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)" |
278 (if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)" |
488 by (auto simp: clamp_def) |
279 by (auto simp: clamp_def) |
489 |
280 |
490 |
281 lemma continuous_on_interval_bcontfunE: |
491 declare [[coercion Rep_bcontfun]] |
282 fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::metric_space" |
492 |
283 assumes "continuous_on {a .. b} f" |
493 lemma ext_cont_cancel[simp]: |
284 obtains g::"'a \<Rightarrow>\<^sub>C 'b" where |
494 fixes x a b :: "'a::euclidean_space" |
285 "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> g x = f x" |
495 assumes x: "x \<in> cbox a b" |
286 "\<And>x. g x = f (clamp a b x)" |
496 and "continuous_on (cbox a b) f" |
287 proof - |
497 shows "ext_cont f a b x = f x" |
288 define g where "g \<equiv> ext_cont f a b" |
498 using assms |
289 have "continuous_on UNIV g" |
499 unfolding ext_cont_def |
290 using assms |
500 proof (subst Abs_bcontfun_inverse[OF clamp_bcontfun]) |
291 by (auto intro!: continuous_on_ext_cont simp: g_def cbox_interval) |
501 show "f (clamp a b x) = f x" |
292 moreover |
502 using x unfolding clamp_def mem_box |
293 have "bounded (range g)" |
503 by (intro arg_cong[where f=f] euclidean_eqI[where 'a='a]) (simp add: not_less) |
294 by (auto simp: g_def ext_cont_def cbox_interval |
504 qed (auto simp: cbox_def) |
295 intro!: compact_interval clamp_bounded compact_imp_bounded[OF compact_continuous_image] assms) |
505 |
296 ultimately |
506 lemma ext_cont_cong: |
297 obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE) |
507 assumes "t0 = s0" |
298 then have "h x = f x" if "a \<le> x" "x \<le> b" for x |
508 and "t1 = s1" |
299 by (auto simp: h[symmetric] g_def cbox_interval that) |
509 and "\<And>t. t \<in> (cbox t0 t1) \<Longrightarrow> f t = g t" |
300 moreover |
510 and "continuous_on (cbox t0 t1) f" |
301 have "h x = f (clamp a b x)" for x |
511 and "continuous_on (cbox s0 s1) g" |
302 by (auto simp: h[symmetric] g_def ext_cont_def) |
512 and ord: "\<And>i. i \<in> Basis \<Longrightarrow> t0 \<bullet> i \<le> t1 \<bullet> i" |
303 ultimately show ?thesis .. |
513 shows "ext_cont f t0 t1 = ext_cont g s0 s1" |
304 qed |
514 unfolding assms ext_cont_def |
305 |
515 using assms clamp_in_interval[OF ord] |
306 lifting_update bcontfun.lifting |
516 by (subst Rep_bcontfun_inject[symmetric]) simp |
307 lifting_forget bcontfun.lifting |
517 |
308 |
518 end |
309 end |