Epsilon Numbers and Cantor Normal Form
Grzegorz Bancerek
Formalized Mathematics, Tome 17 (2009), p. 249-256 / Harvested from The Polish Digital Mathematics Library
Access to full text
Full (PDF)

An epsilon number is a transfinite number which is a fixed point of an exponential map: ωϵ = ϵ. The formalization of the concept is done with use of the tetration of ordinals (Knuth's arrow notation, ↑). Namely, the ordinal indexing of epsilon numbers is defined as follows: [...] and for limit ordinal λ: [...] Tetration stabilizes at ω: [...] Every ordinal number α can be uniquely written as [...] where κ is a natural number, n1, n2, …, nk are positive integers, and β1 > β2 > … > βκ are ordinal numbers (βκ = 0). This decomposition of α is called the Cantor Normal Form of α.

Publié le : 2009-01-01
EUDML-ID : urn:eudml:doc:266687 
@article{bwmeta1.element.doi-10_2478_v10037-009-0032-8,
     author = {Grzegorz Bancerek},
     title = {Epsilon Numbers and Cantor Normal Form},
     journal = {Formalized Mathematics},
     volume = {17},
     year = {2009},
     pages = {249-256},
     language = {en},
     url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_2478_v10037-009-0032-8}
}

Grzegorz Bancerek. Epsilon Numbers and Cantor Normal Form. Formalized Mathematics, Tome 17 (2009) pp. 249-256. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_2478_v10037-009-0032-8/

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. | Zbl 06213858

[2] Grzegorz Bancerek. Increasing and continuous ordinal sequences. Formalized Mathematics, 1(4):711-714, 1990.

[3] Grzegorz Bancerek. König's theorem. Formalized Mathematics, 1(3):589-593, 1990.

[4] Grzegorz Bancerek. Ordinal arithmetics. Formalized Mathematics, 1(3):515-519, 1990.

[5] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.

[6] Grzegorz Bancerek. Sequences of ordinal numbers. Formalized Mathematics, 1(2):281-290, 1990.

[7] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.

[8] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.

[9] Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825-829, 2001.

[10] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.