trans_isEquivalent

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsLittleO.trans_isEquivalent

← MathLib Explorer

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 =o[l] g_1 \Rightarrow g_1 ~[l] g_2 \Rightarrow f =o[l] g_2$$

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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