| changeset 68652 | 1e37b45ce3fb |
| parent 66453 | cc19f7ca2ed6 |
| child 75132 | e349c2da30d2 |
| 68648:371e814af6f0 | 68652:1e37b45ce3fb |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 section \<open>Cardinal Arithmetic\<close> |
8 section \<open>Cardinal Arithmetic\<close> |
9 |
9 |
10 theory Cardinal_Arithmetic |
10 theory Cardinal_Arithmetic |
11 imports HOL.BNF_Cardinal_Arithmetic Cardinal_Order_Relation |
11 imports Cardinal_Order_Relation |
12 begin |
12 begin |
13 |
13 |
14 subsection \<open>Binary sum\<close> |
14 subsection \<open>Binary sum\<close> |
15 |
15 |
16 lemma csum_Cnotzero2: |
16 lemma csum_Cnotzero2: |