limZero_sub_rev

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.limZero_sub_rev

English

LimZero of f−g implies LimZero of g−f (negating a difference preserves the limit-zero property).

Русский

LimZero(f−g) ⇒ LimZero(g−f) (отрицание разности сохраняет стремление к нулю).

LaTeX

$$$\text{LimZero}(f - g) \Rightarrow \text{LimZero}(g - f)$$$

Lean4

theorem limZero_sub_rev {f g : CauSeq β abv} (hfg : LimZero (f - g)) : LimZero (g - f) := by simpa using neg_limZero hfg

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

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

Разделы

Аффилиация

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