isBigOWith_comm

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.isBigOWith_comm

English

If f1 - f2 = O[l] g, then f2 - f1 = O[l] g.

Русский

Если f1 - f2 = O[l] g, то f2 - f1 = O[l] g.

LaTeX

$$$ IsBigO\\ l\\ (f_1 - f_2)\\ g \\Rightarrow IsBigO\\ l\\ (f_2 - f_1)\\ g $$$

Lean4

theorem isBigOWith_comm : IsBigOWith c l (fun x => f₁ x - f₂ x) g ↔ IsBigOWith c l (fun x => f₂ x - f₁ x) g :=
  ⟨IsBigOWith.symm, IsBigOWith.symm⟩

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

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

Разделы

Аффилиация

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