isLittleO — Mathlib

English

Two functions u and v are asymptotically equivalent along l if and only if their difference u − v is little-o of v along l.

Русский

Две функции u и v асимптотически эквивалентны вдоль l тогда и только тогда, когда разность u − v является малым-o по отношению к v вдоль l.

LaTeX

$$$u ~[l] v \iff (u - v) = o[l]\, v$$$

Lean4

theorem isLittleO (h : u ~[l] v) : (u - v) =o[l] v :=
  h

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