mk_eq_mk — Mathlib

English

Let f,g be Cauchy sequences in CauSeq β abv. Then mk f = mk g in the completion if and only if the difference f − g tends to zero, i.e. LimZero (f − g).

Русский

Пусть f,g — последовательности Коши в CauSeq β abv. Тогда mk f = mk g в завершении тогда и только тогда, когда различие f − g tends to zero, то есть LimZero (f − g).

LaTeX

$$$mk\,f = mk\,g \iff \LimZero (f - g)$$$

Lean4

@[simp]
theorem mk_eq_mk (f : CauSeq _ abv) : @Eq (Cauchy abv) ⟦f⟧ (mk f) :=
  rfl

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