FTH0005canonicalv1taureal_archimedean_embedding (theorem)
/-- [I.T42] The Archimedean property: the natural number embedding into TauReal is unbounded. The sequence `fromNat n` is strictly increasing (distinct naturals give non-equivalent TauReals). Under the Cauchy `equiv`, distinctness means the difference sequence does NOT converge to zero. Since `fromNat n` is constant at `n`, the difference `|m - n|` is a fixed nonzero constant, and any small enough `1/(k+1)` tolerance witnesses non-convergence. -/
Formalization
Identifiers
Aliases & legacy IDs
taureal_archimedean_embeddingtaureal-archimedean-embeddingTauLib.BookI.Boundary.ConstructiveReals::taureal_archimedean_embeddingRelease lines
corpus_v2corpus_v3_workingVersion & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.