trans_eventuallyEq

Mathlib.Analysis.Asymptotics.Defs

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

English

If f1 = O[l] g and g1 =ᶠ[l] g2, then f1 = O[l] g2.

Русский

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

LaTeX

$$$ (f = O[l]\, g) \land (g_1 =^\!{l}^{} g_2) \Rightarrow f = O[l]\, g_2 $$$

Lean4

@[trans]
theorem trans_eventuallyEq {f : α → E} {g₁ g₂ : α → F} (h : f =o[l] g₁) (hg : g₁ =ᶠ[l] g₂) : f =o[l] g₂ :=
  h.congr' EventuallyEq.rfl hg

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

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

Разделы

Аффилиация

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