equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *} |
8 header {* Cardinal-Order Relations as Needed by Bounded Natural Functors *} |
9 |
9 |
10 theory BNF_Cardinal_Order_Relation |
10 theory BNF_Cardinal_Order_Relation |
11 imports BNF_Constructions_on_Wellorders |
11 imports Zorn BNF_Constructions_on_Wellorders |
12 begin |
12 begin |
13 |
13 |
14 text{* In this section, we define cardinal-order relations to be minim well-orders |
14 text{* In this section, we define cardinal-order relations to be minim well-orders |
15 on their field. Then we define the cardinal of a set to be {\em some} cardinal-order |
15 on their field. Then we define the cardinal of a set to be {\em some} cardinal-order |
16 relation on that set, which will be unique up to order isomorphism. Then we study |
16 relation on that set, which will be unique up to order isomorphism. Then we study |