mk_eq

Mathlib.Algebra.Order.CauSeq.Completion

URI: https://scilib.ai/kg/mathlib#CauSeq.Completion.mk_eq

English

For any f,g in CauSeq β abv, mk f = mk g iff LimZero (f − g).

Русский

Для любых f,g в CauSeq β abv верно: mk f = mk g тогда и только тогда, когда LimZero (f − g).

LaTeX

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

Lean4

theorem mk_eq {f g : CauSeq _ abv} : mk f = mk g ↔ LimZero (f - g) :=
  Quotient.eq

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru