const_mul_left — Mathlib

English

If c is a unit, then multiplying f by c on the left does not change the little-o relation: (c f) = o_l g iff f = o_l g.

Русский

Если c — единица (обратимый элемент), то левое умножение на c сохраняет отношение малого o: (c f) = o_l(g) эквивалентно f = o_l(g).

LaTeX

$$$\text{IsLittleO}_l\left(c\,f, g\right) \iff \text{IsLittleO}_l\left(f, g\right), \text{ при } c \text{ — единица по норме}.$$$

Lean4

theorem const_mul_left {f : α → R} (h : f =o[l] g) (c : R) : (fun x => c * f x) =o[l] g :=
  (isBigO_const_mul_self c f l).trans_isLittleO h

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