transIsBigOEventuallyEq

Mathlib.Analysis.Asymptotics.Defs

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

English

If f = O[l] g, then (f ∘ k) = O[l'] (g ∘ k) for any k with Tendsto k l' l.

Русский

Если f = O_l(g), то (f ∘ k) = O_l' (g ∘ k) при любом k с Tendsto k l' l.

LaTeX

$$$ IsBigO\ l\; f\; g \to\; (f \circ k) = O[l'] (g \circ k) $$$

Lean4

instance transIsBigOEventuallyEq : @Trans (α → E) (α → F) (α → F) (· =O[l] ·) (· =ᶠ[l] ·) (· =O[l] ·) where
  trans := IsBigO.trans_eventuallyEq

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

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

Разделы

Аффилиация

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