transIsLittleOIsBigO

Mathlib.Analysis.Asymptotics.Defs

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

English

There is a transitive composition of Big-O relations: if f =O_l g and g =O_l k, then 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 transIsLittleOIsBigO : @Trans (α → E) (α → F) (α → G') (· =o[l] ·) (· =O[l] ·) (· =o[l] ·) where
  trans := IsLittleO.trans_isBigO

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

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

Разделы

Аффилиация

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