add_isLittleO — Mathlib

English

If u is asymptotically equivalent to v along l and w is little-o of v along l, then u + w is asymptotically equivalent to v along l.

Русский

Если функции u и v эквивалентны по ленте l, и w = o_l(v), то u + w эквивалентна v по l.

LaTeX

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

Lean4

theorem add_isLittleO (huv : u ~[l] v) (hwv : w =o[l] v) : u + w ~[l] v := by
  simpa only [IsEquivalent, add_sub_right_comm] using huv.add hwv

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