transIsLittleOIsLittleO

Mathlib.Analysis.Asymptotics.Defs

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

English

There is a transitive composition of Big-O relations: f =O_l g and g =O_l k yields f =O_l k.

Русский

Существует транзитивная компоновка отношений Big-O: f =O_l g и g =O_l k дают f =O_l k.

LaTeX

$$$f =O_l g \land g =O_l k \Rightarrow f =O_l k$$$

Lean4

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

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

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

Разделы

Аффилиация

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