English
A Cauchy sequence in a uniform space is a function u from a preorder β to α such that its image under the atTop map is a Cauchy filter on α.
Русский
Коши-последовательность в униформном пространстве — это функция u: β → α, чье изображение через переход к бесконечности (atTop) образует Коши-фильтр на α.
LaTeX
$$$\\text{CauchySeq}(u) \\quad\\text{means}\\quad Cauchy(\\operatorname{atTop}.map(u)).$$$
Lean4
/-- Cauchy sequences. Usually defined on ℕ, but often it is also useful to say that a function
defined on ℝ is Cauchy at +∞ to deduce convergence. Therefore, we define it in a type class that
is general enough to cover both ℕ and ℝ, which are the main motivating examples. -/
def CauchySeq [Preorder β] (u : β → α) :=
Cauchy (atTop.map u)
