# Formal limits are genuine limits

Suppose that \( (a_n)_{n=1}^{\infty} \) is a Cauchy sequence of rational numbers (defined for reals). Then \( (a_n)_{n=1}^{\infty} \) converges to \( LIM_{n\to\infty}a_n \), i.e.

The real defined by the Cauchy sequence is equal to the real to which the matching sequence of reals converges to.

Going forward, this equality allows limits to be used inplace of formal limits. Underneath, however, each real is still defined as a formal limit of rationals.

This masking of the foundations was similarly undertaken for rationals, integers and natural numbers. The pair of integers combined with '//' to make a rational, the pair of natural numbers combined with '—' to make an integer, and the increment operation—all were masked by subsequently defined operations.

## Context

*subsumption of formal limits*