equivCauchy — Mathlib

English

The real numbers are isomorphic to the Cauchy completion of the rationals with the standard absolute value.

Русский

Действительные числа изоморфны дополнению Коши рациональных чисел по стандартной абсолютной величине.

LaTeX

$$$$\mathbb{R} \cong \mathrm{CauSeq.Completion.Cauchy}(|\cdot|).$$$$

Lean4

/-- The real numbers are isomorphic to the quotient of Cauchy sequences on the rationals. -/
def equivCauchy : ℝ ≃ CauSeq.Completion.Cauchy (abs : ℚ → ℚ) :=
  ⟨Real.cauchy, Real.ofCauchy, fun ⟨_⟩ => rfl, fun _ => rfl⟩
    -- irreducible doesn't work for instances: https://github.com/leanprover-community/lean/issues/511

Похожие утверждения