trans_le

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsBigO.trans_le

English

If f = O_l g and g = o_l k with c > 0, then f = o_l k.

Русский

Если f = O_l g и g = o_l k при c > 0, тогда f = o_l k.

LaTeX

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

Lean4

theorem trans_le (hfg : f =O[l] g') (hgk : ∀ x, ‖g' x‖ ≤ ‖k x‖) : f =O[l] k :=
  hfg.trans (isBigO_of_le l hgk)

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

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

Разделы

Аффилиация

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