mk_eq — Mathlib

English

Two Cauchy sequences represent the same real number precisely when they are equivalent in the CauSeq sense.

Русский

Две последовательности Коши представляют одно и то же число действительное тогда и только тогда, когда они эквивалентны по определению CauSeq.

LaTeX

$$$$\\operatorname{mk}(f) = \\operatorname{mk}(g) \\iff f \\approx g.$$$$

Lean4

theorem mk_eq {f g : CauSeq ℚ abs} : mk f = mk g ↔ f ≈ g :=
  ext_cauchy_iff.trans CauSeq.Completion.mk_eq

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