trans_isBigO

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsEquivalent.trans_isBigO

English

If f ~_l g1 and g1 =O_l g2, then f =O_l g2.

Русский

Если f эквивалентно g1 по l и g1 = O_l g2, тогда f = O_l g2.

LaTeX

$$f ~_l g_1 \Rightarrow g_1 =O_l g_2 \Rightarrow f =O_l g_2$$

Lean4

@[trans]
theorem trans_isBigO {f g₁ : α → β} {g₂ : α → β₂} (h : f ~[l] g₁) (h₂ : g₁ =O[l] g₂) : f =O[l] g₂ :=
  IsBigO.trans h.isBigO h₂

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

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

Разделы

Аффилиация

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