Cauchy sequences of reals
We can define Cauchy sequences of reals in the same way as was done for rationals. For rationals, many ideas of closeness were introduced separately before reaching Cauchy sequences. This card compresses all of the ideas for reals.Distance and ε-close reals
Let \( a \) and \( b \) be two real numbers. Define their distance \( d(a,b) \) to be \( d(a,b) := |a - b| \). Let \( \varepsilon > 0 \) be a real. The two reals \( a \) and \( b \) are said to be ε-close if \( d(a,b) \le \varepsilon \).
Sequence of reals
A sequences of reals is denoted in the same way as a sequences of rationals: \( (a_n)_{n=m}^{\infty} \) represents a function \( f \) from the set \( \{y \in \mathbb{Z} : y \ge m \} \) to the set of reals, where \( a_n := f(n) \).
ε-steady sequence of reals
A sequence \( (a_n)_{n=N}^{\infty} \) of reals is said to be ε-steady if \( a_j \) and \( a_k \) are ε-close for all \( j, k \ge N \).
Eventually ε-steady
A sequence \( (a_n)_{n=m}^{\infty} \) of reals is said to be eventually ε-steady if \( (a_n)_{n=N}^{\infty} \) is ε-steady for some integer \( N \ge m \).
Cauchy sequence
A sequence \( (a_n)_{n=m}^{\infty} \) of reals is said to be a Cauchy sequence if it is eventually ε-steady for every real \( \varepsilon > 0 \).
Cauchy sequences of reals → convergence of sequences of reals → uniqueness of convergence → limit, the definition → subsumption of formal limits