English
There is a canonical embedding of Cauchy sequences of rationals into the real numbers, sending each sequence to its limit.
Русский
Существует каноническое вложение последовательностей Коши из рациональных чисел в множество действительных чисел, отправляющее последовательность в её предел.
LaTeX
$$$$\\operatorname{mk}: \\mathrm{CauSeq}(\\mathbb{Q}, |\\cdot|) \\to \\mathbb{R}$$ is the map sending a Cauchy sequence to its real limit.$$
Lean4
/-- Make a real number from a Cauchy sequence of rationals (by taking the equivalence class). -/
def mk (x : CauSeq ℚ abs) : ℝ :=
⟨CauSeq.Completion.mk x⟩
