isBigO_refl_left

Mathlib.Analysis.Asymptotics.Defs

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

English

Similarly, f′ − f′ = 0 implies (f′ − f′) = o_l(g′).

Русский

Аналогично, нулевая функция принадлежит little-o: f′ − f′ = o_l(g′).

LaTeX

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

Lean4

theorem isBigO_refl_left : (fun x => f' x - f' x) =O[l] g' :=
  (isBigO_zero g' l).congr_left fun _x => (sub_self _).symm

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

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

Разделы

Аффилиация

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