src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 67135 1a94352812f4
parent 66827 c94531b5007d
child 67167 88d1c9d86f48
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Dec 04 23:10:52 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Dec 05 12:14:36 2017 +0100
     1.3 @@ -367,6 +367,10 @@
     1.4    "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) holomorphic_on s"
     1.5    unfolding holomorphic_on_def by (metis field_differentiable_sum)
     1.6  
     1.7 +lemma holomorphic_on_prod [holomorphic_intros]:
     1.8 +  "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. prod (\<lambda>i. f i x) I) holomorphic_on s"
     1.9 +  by (induction I rule: infinite_finite_induct) (auto intro: holomorphic_intros)
    1.10 +
    1.11  lemma holomorphic_pochhammer [holomorphic_intros]:
    1.12    "f holomorphic_on A \<Longrightarrow> (\<lambda>s. pochhammer (f s) n) holomorphic_on A"
    1.13    by (induction n) (auto intro!: holomorphic_intros simp: pochhammer_Suc)