trans_eventuallyEq

Mathlib.Analysis.Asymptotics.Defs

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

English

f = O[map k l] g iff (f ∘ k) = O[l] (g ∘ k).

Русский

f = O по отображению map k l g эквивалентно (f ∘ k) = O[l] (g ∘ k).

LaTeX

$$$ f = O[map\ k\ l]\, g \;\Longleftrightarrow\; (f\circ k) = O[l]\, (g\circ k) $$$

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