transIsLittleOEventuallyEq

Mathlib.Analysis.Asymptotics.Defs

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

← MathLib Explorer

English

If f1 = o[l] g and f1 ≡ f2, g1 ≡ g2 along l, then f2 = o[l] g2.

Русский

Если f1 = o_l(g) и f1 ≡ f2, g1 ≡ g2 вдоль l, тогда f2 = o_l(g2).

LaTeX

$$$ (f_1 = o[l]\, g) \land (f_1 =^\!{l}^{} f_2) \land (g_1 =^\!{l}^{} g_2) \Rightarrow f_2 = o[l]\, g_2 $$$

Lean4

instance transIsLittleOEventuallyEq : @Trans (α → E) (α → F) (α → F) (· =o[l] ·) (· =ᶠ[l] ·) (· =o[l] ·) where
  trans := IsLittleO.trans_eventuallyEq

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

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

Разделы

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

Аффилиация

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