symm

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsBigO.symm

English

Same symmetry property for little-o as above.

Русский

Та же симметрия для малого o, как выше.

LaTeX

$$ (f1 - f2) = o_l g \leftrightarrow (f2 - f1) = o_l g$$

Lean4

theorem symm (h : (fun x => f₁ x - f₂ x) =O[l] g) : (fun x => f₂ x - f₁ x) =O[l] g :=
  h.neg_left.congr_left fun _x => neg_sub _ _

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

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

Разделы

Аффилиация

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