equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 section \<open>Well-Order Embeddings\<close> |
8 section \<open>Well-Order Embeddings\<close> |
9 |
9 |
10 theory Wellorder_Embedding |
10 theory Wellorder_Embedding |
11 imports BNF_Wellorder_Embedding Fun_More Wellorder_Relation |
11 imports HOL.BNF_Wellorder_Embedding Fun_More Wellorder_Relation |
12 begin |
12 begin |
13 |
13 |
14 subsection \<open>Auxiliaries\<close> |
14 subsection \<open>Auxiliaries\<close> |
15 |
15 |
16 lemma UNION_bij_betw_ofilter: |
16 lemma UNION_bij_betw_ofilter: |