congr_right

Mathlib.Analysis.Asymptotics.Defs

URI: https://scilib.ai/kg/mathlib#Asymptotics.IsLittleO.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