equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* Well-Order Embeddings as Needed by Bounded Natural Functors *} |
8 header {* Well-Order Embeddings as Needed by Bounded Natural Functors *} |
9 |
9 |
10 theory BNF_Wellorder_Embedding |
10 theory BNF_Wellorder_Embedding |
11 imports Zorn BNF_Wellorder_Relation |
11 imports Hilbert_Choice BNF_Wellorder_Relation |
12 begin |
12 begin |
13 |
13 |
14 text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and |
14 text{* In this section, we introduce well-order {\em embeddings} and {\em isomorphisms} and |
15 prove their basic properties. The notion of embedding is considered from the point |
15 prove their basic properties. The notion of embedding is considered from the point |
16 of view of the theory of ordinals, and therefore requires the source to be injected |
16 of view of the theory of ordinals, and therefore requires the source to be injected |