congr_right

Mathlib.Analysis.Asymptotics.Defs

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

English

If f = O_l(g1) and g1 = g2 pointwise, then f = O_l(g2).

Русский

Если f = O_l(g1) и g1(x) = g2(x) для всех x, тогда f = O_l(g2).

LaTeX

$$$ (f = O[l]\, g_1) \land (\forall x,\; g_1(x)=g_2(x)) \Rightarrow f = O[l]\, g_2 $$$

Lean4

theorem congr_right (h : f =O[l] g₁) (hg : ∀ x, g₁ x = g₂ x) : f =O[l] g₂ :=
  h.congr (fun _ => rfl) hg

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

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

Разделы

Аффилиация

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