isEquivalent

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

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

English

If u - v = o_l v, then u is asymptotically equivalent to v.

Русский

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

LaTeX

$$$ (u - v) = o_{l} v \\Rightarrow u \\sim_{l} v $$$

Lean4

theorem isEquivalent (huv : (u - v) =o[l] v) : u ~[l] v :=
  huv

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

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

Разделы

Аффилиация

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