src/HOL/Analysis/Infinite_Products.thy
changeset 68127 137d5d0112bb
parent 68076 315043faa871
child 68136 f022083489d0
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Wed May 09 07:48:54 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Wed May 09 14:07:19 2018 +0100
     1.3 @@ -688,4 +688,31 @@
     1.4      by (simp add: convergent_prod_def)
     1.5  qed
     1.6  
     1.7 +lemma has_prod_If_finite_set:
     1.8 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
     1.9 +  shows "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 1) has_prod (\<Prod>r\<in>A. f r)"
    1.10 +  using has_prod_finite[of A "(\<lambda>r. if r \<in> A then f r else 1)"]
    1.11 +  by simp
    1.12 +
    1.13 +lemma has_prod_If_finite:
    1.14 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.15 +  shows "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 1) has_prod (\<Prod>r | P r. f r)"
    1.16 +  using has_prod_If_finite_set[of "{r. P r}"] by simp
    1.17 +
    1.18 +lemma convergent_prod_If_finite_set[simp, intro]:
    1.19 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.20 +  shows "finite A \<Longrightarrow> convergent_prod (\<lambda>r. if r \<in> A then f r else 1)"
    1.21 +  by (simp add: convergent_prod_finite)
    1.22 +
    1.23 +lemma convergent_prod_If_finite[simp, intro]:
    1.24 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.25 +  shows "finite {r. P r} \<Longrightarrow> convergent_prod (\<lambda>r. if P r then f r else 1)"
    1.26 +  using convergent_prod_def has_prod_If_finite has_prod_def by fastforce
    1.27 +
    1.28 +lemma has_prod_single:
    1.29 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.30 +  shows "(\<lambda>r. if r = i then f r else 1) has_prod f i"
    1.31 +  using has_prod_If_finite[of "\<lambda>r. r = i"] by simp
    1.32 +
    1.33 +
    1.34  end