transIsBigOIsEquivalent

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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

English

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

Русский

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

LaTeX

$${f : α → β₂}{g1 g2 : α → β} (h : f =O[l] g1) (h2 : g1 ~[l] g2) : f =O[l] g2$$

Lean4

instance transIsBigOIsEquivalent : @Trans (α → β₂) (α → β) (α → β) (IsBigO l) (IsEquivalent l) (IsBigO l) where
  trans := IsBigO.trans_isEquivalent

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

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

Разделы

Аффилиация

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