mathlib

b3ff79ae - feat(topology/uniform_space/uniform_convergence): Uniform Cauchy sequences (#14003)

feat(topology/uniform_space/uniform_convergence): Uniform Cauchy sequences (#14003) A sequence of functions `f_n` is pointwise Cauchy if `∀x ∀ε ∃N ∀(m, n) > N` we have `|f_m x - f_n x| < ε`. A sequence of functions is _uniformly_ Cauchy if `∀ε ∃N ∀(m, n) > N ∀x` we have `|f_m x - f_n x| < ε`. As a sequence of functions is pointwise Cauchy if (and when the underlying space is complete, only if) the sequence converges, a sequence of functions is uniformly Cauchy if (and when the underlying space is complete, only if) the sequence uniformly converges. (Note that the parenthetical is not directly covered by this commit, but is an easy consequence of two of its lemmas.) This notion is commonly used to bootstrap convergence into uniform convergence.