src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 68296 69d680e94961
parent 68255 009f783d1bac
child 68721 53ad5c01be3f
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat May 26 10:11:11 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sat May 26 22:11:55 2018 +0100
     1.3 @@ -47,26 +47,6 @@
     1.4  lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = ( * ) 1"
     1.5    by auto
     1.6  
     1.7 -lemma continuous_mult_left:
     1.8 -  fixes c::"'a::real_normed_algebra"
     1.9 -  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. c * f x)"
    1.10 -by (rule continuous_mult [OF continuous_const])
    1.11 -
    1.12 -lemma continuous_mult_right:
    1.13 -  fixes c::"'a::real_normed_algebra"
    1.14 -  shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x * c)"
    1.15 -by (rule continuous_mult [OF _ continuous_const])
    1.16 -
    1.17 -lemma continuous_on_mult_left:
    1.18 -  fixes c::"'a::real_normed_algebra"
    1.19 -  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. c * f x)"
    1.20 -by (rule continuous_on_mult [OF continuous_on_const])
    1.21 -
    1.22 -lemma continuous_on_mult_right:
    1.23 -  fixes c::"'a::real_normed_algebra"
    1.24 -  shows "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x * c)"
    1.25 -by (rule continuous_on_mult [OF _ continuous_on_const])
    1.26 -
    1.27  lemma uniformly_continuous_on_cmul_right [continuous_intros]:
    1.28    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
    1.29    shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f x * c)"