equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Cardinal-Order Relations *} |
8 header {* Cardinal-Order Relations *} |
9 |
9 |
10 theory Cardinal_Order_Relation |
10 theory Cardinal_Order_Relation |
11 imports Cardinal_Order_Relation_LFP Constructions_on_Wellorders |
11 imports Cardinal_Order_Relation_FP Constructions_on_Wellorders |
12 begin |
12 begin |
13 |
13 |
14 declare |
14 declare |
15 card_order_on_well_order_on[simp] |
15 card_order_on_well_order_on[simp] |
16 card_of_card_order_on[simp] |
16 card_of_card_order_on[simp] |
134 qed |
134 qed |
135 |
135 |
136 |
136 |
137 subsection {* Cardinals versus set operations on arbitrary sets *} |
137 subsection {* Cardinals versus set operations on arbitrary sets *} |
138 |
138 |
139 lemma infinite_Pow: |
139 lemma card_of_set_type[simp]: "|UNIV::'a set| <o |UNIV::'a set set|" |
140 assumes "infinite A" |
|
141 shows "infinite (Pow A)" |
|
142 proof- |
|
143 have "|A| \<le>o |Pow A|" by (metis card_of_Pow ordLess_imp_ordLeq) |
|
144 thus ?thesis by (metis assms finite_Pow_iff) |
|
145 qed |
|
146 |
|
147 corollary card_of_set_type[simp]: "|UNIV::'a set| <o |UNIV::'a set set|" |
|
148 using card_of_Pow[of "UNIV::'a set"] by simp |
140 using card_of_Pow[of "UNIV::'a set"] by simp |
149 |
141 |
150 lemma card_of_Un1[simp]: |
142 lemma card_of_Un1[simp]: |
151 shows "|A| \<le>o |A \<union> B| " |
143 shows "|A| \<le>o |A \<union> B| " |
152 using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce |
144 using inj_on_id[of A] card_of_ordLeq[of A _] by fastforce |