Registry · Theorem I.T42 established formalized

I.T42 — Archimedean Property

The Archimedean property: the natural number embedding into TauReal is unbounded and injective. For any n < m, fromNat(m) is not equivalent to fromNat(n).

Book I Part 17 Ch. 76

Dependency Graph

Depends on (1)

I.D84

Lean Formalization

Module: TauLib.BookI.Boundary.ConstructiveReals

Symbol: Tau.Boundary.taureal_archimedean_embedding