trans_isLittleO

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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

English

If f ~_l g and g =o_l g2, then f =o_l g2.

Русский

Если f эквивалентно g по l и g = o_l g2, то f = o_l g2.

LaTeX

$$f ~_l g \Rightarrow g =o[l] g_2 \Rightarrow f =o[l] g_2$$

Lean4

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

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

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

Разделы

Аффилиация

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