add_isEquivalent

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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

English

If u = o_l w and v is asymptotically equivalent to w, then u + v is asymptotically equivalent to w.

Русский

Если u = o_l w и v эквивалентно w по l, то u + v эквивалентно w по l.

LaTeX

$$$ (u = o_{l} w) \\land (v \\sim_{l} w) \\Rightarrow (u + v) \\sim_{l} w $$$

Lean4

theorem add_isEquivalent (hu : u =o[l] w) (hv : v ~[l] w) : u + v ~[l] w :=
  add_comm v u ▸ hv.add_isLittleO hu

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

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

Разделы

Аффилиация

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