| changeset 68652 | 1e37b45ce3fb |
| parent 66453 | cc19f7ca2ed6 |
| child 76948 | f33df7529fed |
| 68648:371e814af6f0 | 68652:1e37b45ce3fb |
|---|---|
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 HOL.BNF_Wellorder_Embedding Fun_More Wellorder_Relation |
11 imports 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: |