equal
deleted
inserted
replaced
650 hence "|A Un B| <o |?C|" using INF |
650 hence "|A Un B| <o |?C|" using INF |
651 card_of_Un_ordLess_infinite by blast |
651 card_of_Un_ordLess_infinite by blast |
652 thus ?thesis using 1 ordLess_ordIso_trans by blast |
652 thus ?thesis using 1 ordLess_ordIso_trans by blast |
653 qed |
653 qed |
654 |
654 |
|
655 lemma ordLeq_finite_Field: |
|
656 assumes "r \<le>o s" and "finite (Field s)" |
|
657 shows "finite (Field r)" |
|
658 by (metis assms card_of_mono2 card_of_ordLeq_infinite) |
|
659 |
|
660 lemma ordIso_finite_Field: |
|
661 assumes "r =o s" |
|
662 shows "finite (Field r) \<longleftrightarrow> finite (Field s)" |
|
663 by (metis assms ordIso_iff_ordLeq ordLeq_finite_Field) |
|
664 |
655 |
665 |
656 subsection {* Cardinals versus set operations involving infinite sets *} |
666 subsection {* Cardinals versus set operations involving infinite sets *} |
657 |
667 |
658 lemma finite_iff_cardOf_nat: |
668 lemma finite_iff_cardOf_nat: |
659 "finite A = ( |A| <o |UNIV :: nat set| )" |
669 "finite A = ( |A| <o |UNIV :: nat set| )" |