sub_isLittleO

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsBigOWith.sub_isLittleO

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$ (f_1 =O[l] g) \\land (f_2 =O[l] g) \\Rightarrow (f_1 - f_2) =O[l] g $$$

Lean4

theorem sub_isLittleO (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : f₂ =o[l] g) (hc : c₁ < c₂) :
    IsBigOWith c₂ l (fun x => f₁ x - f₂ x) g := by simpa only [sub_eq_add_neg] using h₁.add_isLittleO h₂.neg_left hc

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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