changeset 16417 | 9bc16273c2d4 |
parent 13339 | 0f89104dd377 |
child 24893 | b8ef7afe3a6b |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
3 Author: Krzysztof Grabczewski |
3 Author: Krzysztof Grabczewski |
4 |
4 |
5 Hartog's function. |
5 Hartog's function. |
6 *) |
6 *) |
7 |
7 |
8 theory Hartog = AC_Equiv: |
8 theory Hartog imports AC_Equiv begin |
9 |
9 |
10 constdefs |
10 constdefs |
11 Hartog :: "i => i" |
11 Hartog :: "i => i" |
12 "Hartog(X) == LEAST i. ~ i \<lesssim> X" |
12 "Hartog(X) == LEAST i. ~ i \<lesssim> X" |
13 |
13 |