isLittleO_refl_left

Mathlib.Analysis.Asymptotics.Defs

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

English

As above, the zero difference yields a trivial Little-O bound.

Русский

Как выше, нулевая разность удовлетворяет тривиальному ограничению Little-O.

LaTeX

$$$(f'-f')=o[l]\\,g'$$$

Lean4

theorem isLittleO_refl_left : (fun x => f' x - f' x) =o[l] g' :=
  (isLittleO_zero g' l).congr_left fun _x => (sub_self _).symm

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

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

Разделы

Аффилиация

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