448 proof (cases "finite s") |
448 proof (cases "finite s") |
449 case True then show ?thesis using assms |
449 case True then show ?thesis using assms |
450 by (induct s rule: finite_induct) auto |
450 by (induct s rule: finite_induct) auto |
451 next |
451 next |
452 case False then show ?thesis using assms |
452 case False then show ?thesis using assms |
453 by (metis Reals_0 setsum_infinite) |
453 by (metis Reals_0 setsum.infinite) |
454 qed |
454 qed |
455 |
455 |
456 lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>" |
456 lemma setprod_in_Reals: assumes "\<And>i. i \<in> s \<Longrightarrow> f i \<in> \<real>" shows "setprod f s \<in> \<real>" |
457 proof (cases "finite s") |
457 proof (cases "finite s") |
458 case True then show ?thesis using assms |
458 case True then show ?thesis using assms |
459 by (induct s rule: finite_induct) auto |
459 by (induct s rule: finite_induct) auto |
460 next |
460 next |
461 case False then show ?thesis using assms |
461 case False then show ?thesis using assms |
462 by (metis Reals_1 setprod_infinite) |
462 by (metis Reals_1 setprod.infinite) |
463 qed |
463 qed |
464 |
464 |
465 lemma Reals_induct [case_names of_real, induct set: Reals]: |
465 lemma Reals_induct [case_names of_real, induct set: Reals]: |
466 "q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q" |
466 "q \<in> \<real> \<Longrightarrow> (\<And>r. P (of_real r)) \<Longrightarrow> P q" |
467 by (rule Reals_cases) auto |
467 by (rule Reals_cases) auto |