src/HOL/Analysis/Infinite_Products.thy
 changeset 73004 cf14976d4fdb parent 71827 5e315defb038 child 73005 83b114a6545f
equal inserted replaced
73003:ea0108cefc86 73004:cf14976d4fdb
`  1340 lemma has_prod_one_iff_shift:`
`  1340 lemma has_prod_one_iff_shift:`
`  1341   assumes "\<And>i. i < n \<Longrightarrow> f i = 1"`
`  1341   assumes "\<And>i. i < n \<Longrightarrow> f i = 1"`
`  1342   shows "(\<lambda>i. f (i+n)) has_prod a \<longleftrightarrow> (\<lambda>i. f i) has_prod a"`
`  1342   shows "(\<lambda>i. f (i+n)) has_prod a \<longleftrightarrow> (\<lambda>i. f i) has_prod a"`
`  1343   by (simp add: assms has_prod_iff_shift)`
`  1343   by (simp add: assms has_prod_iff_shift)`
`  1344 `
`  1344 `
`  1345 lemma convergent_prod_iff_shift:`
`  1345 lemma convergent_prod_iff_shift [simp]:`
`  1346   shows "convergent_prod (\<lambda>i. f (i + n)) \<longleftrightarrow> convergent_prod f"`
`  1346   shows "convergent_prod (\<lambda>i. f (i + n)) \<longleftrightarrow> convergent_prod f"`
`  1347   apply safe`
`  1347   apply safe`
`  1348   using convergent_prod_offset apply blast`
`  1348   using convergent_prod_offset apply blast`
`  1349   using convergent_prod_ignore_initial_segment convergent_prod_def by blast`
`  1349   using convergent_prod_ignore_initial_segment convergent_prod_def by blast`
`  1350 `
`  1350 `