isLittleO_id_one

Mathlib.Analysis.Asymptotics.Lemmas

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

English

If f^n = O_l g^n with n ≠ 0, then f = O_l g.

Русский

Если f^n = O_l g^n при n ≠ 0, то f = O_l g.

LaTeX

$$$ \text{If } (f^n) =O[l] (g^n) \text{ with } n \neq 0, \text{ then } f =O[l] g. $$$

Lean4

theorem isLittleO_id_one [One F''] [NeZero (1 : F'')] : (fun x : E'' => x) =o[𝓝 0] (1 : E'' → F'') :=
  isLittleO_id_const one_ne_zero

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

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

Разделы

Аффилиация

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