Uniformly Cauchy sequence of functions

Definition

Let $S$ be a set and let $f_n \colon S \to \mathbb{R}$ for $n \ge 1$. The sequence $(f_n)$ is uniformly Cauchy on $S$ if for every $\varepsilon > 0$ there is $N$ such that $$|f_n(x) - f_m(x)| < \varepsilon \quad \text{for all } m, n \ge N \text{ and all } x \in S.$$

Remarks

For each $x$, the sequence $(f_n(x))$ is then a Cauchy sequence. So it has a limit $f(x)$, by the Cauchy criterion. A sequence of real functions is uniformly Cauchy on $S$ if and only if it converges uniformly on $S$. This criterion proves uniform convergence without knowing the limit. Mathlib defines it as UniformCauchySeqOn.

Explanations

L1 human

A uniformly Cauchy sequence has graphs that get close to each other, uniformly in $x$. Such a sequence always converges uniformly to some function.