# HG changeset patch # User immler # Date 1566940348 -7200 # Node ID 191bb458b95c465380afcd021d218742126c91c6 # Parent d9a71b41de497a21c28337ced85dd39949f23efb removed unused lemma, generalized, reduced dependencies diff -r d9a71b41de49 -r 191bb458b95c src/HOL/Analysis/Bounded_Continuous_Function.thy --- a/src/HOL/Analysis/Bounded_Continuous_Function.thy Tue Aug 27 22:43:19 2019 +0200 +++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy Tue Aug 27 23:12:28 2019 +0200 @@ -2,7 +2,8 @@ theory Bounded_Continuous_Function imports - Henstock_Kurzweil_Integration + Topology_Euclidean_Space + Uniform_Limit begin subsection \Definition\ @@ -292,27 +293,22 @@ subsection\<^marker>\tag unimportant\ \(bounded) continuous extenstion\ -lemma integral_clamp: - "integral {t0::real..clamp t0 t1 x} f = - (if x < t0 then 0 else if x \ t1 then integral {t0..x} f else integral {t0..t1} f)" - by (auto simp: clamp_def) - -lemma continuous_on_interval_bcontfunE: - fixes f::"'a::ordered_euclidean_space \ 'b::metric_space" - assumes "continuous_on {a .. b} f" +lemma continuous_on_cbox_bcontfunE: + fixes f::"'a::euclidean_space \ 'b::metric_space" + assumes "continuous_on (cbox a b) f" obtains g::"'a \\<^sub>C 'b" where - "\x. a \ x \ x \ b \ g x = f x" + "\x. x \ cbox a b \ g x = f x" "\x. g x = f (clamp a b x)" proof - define g where "g \ ext_cont f a b" have "g \ bcontfun" using assms - by (auto intro!: continuous_on_ext_cont simp: g_def cbox_interval bcontfun_def) - (auto simp: g_def ext_cont_def cbox_interval - intro!: compact_interval clamp_bounded compact_imp_bounded[OF compact_continuous_image] assms) + by (auto intro!: continuous_on_ext_cont simp: g_def bcontfun_def) + (auto simp: g_def ext_cont_def + intro!: clamp_bounded compact_imp_bounded[OF compact_continuous_image] assms) then obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE) - then have "h x = f x" if "a \ x" "x \ b" for x - by (auto simp: h[symmetric] g_def cbox_interval that) + then have "h x = f x" if "x \ cbox a b" for x + by (auto simp: h[symmetric] g_def that) moreover have "h x = f (clamp a b x)" for x by (auto simp: h[symmetric] g_def ext_cont_def)