equal
deleted
inserted
replaced
353 by (subst UNIV_Plus_UNIV [symmetric]) (rule finite_Plus_iff) |
353 by (subst UNIV_Plus_UNIV [symmetric]) (rule finite_Plus_iff) |
354 |
354 |
355 lemma finite_SigmaI [simp, intro]: |
355 lemma finite_SigmaI [simp, intro]: |
356 "finite A \<Longrightarrow> (\<And>a. a\<in>A \<Longrightarrow> finite (B a)) ==> finite (SIGMA a:A. B a)" |
356 "finite A \<Longrightarrow> (\<And>a. a\<in>A \<Longrightarrow> finite (B a)) ==> finite (SIGMA a:A. B a)" |
357 by (unfold Sigma_def) blast |
357 by (unfold Sigma_def) blast |
|
358 |
|
359 lemma finite_SigmaI2: |
|
360 assumes "finite {x\<in>A. B x \<noteq> {}}" |
|
361 and "\<And>a. a \<in> A \<Longrightarrow> finite (B a)" |
|
362 shows "finite (Sigma A B)" |
|
363 proof - |
|
364 from assms have "finite (Sigma {x\<in>A. B x \<noteq> {}} B)" by auto |
|
365 also have "Sigma {x:A. B x \<noteq> {}} B = Sigma A B" by auto |
|
366 finally show ?thesis . |
|
367 qed |
358 |
368 |
359 lemma finite_cartesian_product: |
369 lemma finite_cartesian_product: |
360 "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A \<times> B)" |
370 "finite A \<Longrightarrow> finite B \<Longrightarrow> finite (A \<times> B)" |
361 by (rule finite_SigmaI) |
371 by (rule finite_SigmaI) |
362 |
372 |