isBigOWith_of_le'

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.isBigOWith_of_le'

English

Little-o transitivity: if f = o_l g and g = o_l k, then f = o_l k.

Русский

Транзитивность Little-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

theorem isBigOWith_of_le' (hfg : ∀ x, ‖f x‖ ≤ c * ‖g x‖) : IsBigOWith c l f g :=
  IsBigOWith.of_bound <| univ_mem' hfg

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

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

Разделы

Аффилиация

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