isBigOWith_zero'

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.isBigOWith_zero'

English

If (f1 − f2) = O_l(g), then f1 = O_l(g) ↔ f2 = O_l(g).

Русский

Если (f1 − f2) = O_l(g), то f1 = O_l(g) тогда и только тогда, когда f2 = O_l(g).

LaTeX

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

Lean4

theorem isBigOWith_zero' : IsBigOWith 0 l (fun _x => (0 : E')) g :=
  IsBigOWith.of_bound <| univ_mem' fun x => by simp

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

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

Разделы

Аффилиация

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